1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v
index 28b2d6fb9..dce4c64e8 100755
--- a/theories/Sets/Finite_sets.v
+++ b/theories/Sets/Finite_sets.v
@@ -59,8 +59,8 @@ Lemma cardinal_invert :
    match p with
    | O => X = Empty_set U
    | S n =>
-        exists A : _
-       | ( exists x : _ | X = Add U A x /\ ~ In U A x /\ cardinal U A n)
+        exists A : _,
+         (exists x : _, X = Add U A x /\ ~ In U A x /\ cardinal U A n)
    end.
 Proof.
 induction 1; simpl in |- *; auto.
@@ -78,4 +78,4 @@ Proof.
 intros X p C; elim C; simpl in |- *; trivial with sets.
 Qed.
 
-End Ensembles_finis_facts.
-\ No newline at end of file
+End Ensembles_finis_facts.