[B] Use Im in statements about Family Complement

This makes it easier to apply lemmas related to `Im`, thus equational
resoning becomes easier. The statement useng `EnsembleSpec` is a bit
harder to use in proofs.

`Complement_FamilyIntersection` and `Complement_FamilyUnion` are
affected.

theories/Topology/TopologicalSpaces.v

@@ -181,9 +181,8 @@ red.
 rewrite Complement_FamilyIntersection.
 apply open_family_union.
 intros.
-destruct H0.
-pose proof (H _ H0).
-rewrite Complement_Complement in H1; assumption.
+destruct H0. subst.
+apply H, H0.
 Qed.
 
 Lemma closed_indexed_intersection: forall {X:TopologicalSpace}
@@ -243,9 +242,8 @@ refine (Build_TopologicalSpace X
 - intros.
   rewrite Complement_FamilyUnion.
   apply closedP_family_intersection.
-  destruct 1.
-  rewrite <- Complement_Complement.
-  apply H; trivial.
+  destruct 1. subst.
+  auto.
 - intros.
   rewrite Complement_Intersection.
   apply closedP_union2; trivial.

theories/ZornsLemma/Families.v

@@ -90,8 +90,7 @@ Qed.
 
 Lemma Complement_FamilyIntersection: forall F:Family T,
     Complement (FamilyIntersection F) =
-    FamilyUnion [ S:Ensemble T |
-                  In F (Complement S)].
+    FamilyUnion (Im F Complement).
 Proof.
 intros.
 apply Extensionality_Ensembles; split; red; intros.
@@ -104,35 +103,31 @@ apply Extensionality_Ensembles; split; red; intros.
   red; intro.
   contradict H0.
   exists (Complement S).
-  + constructor. rewrite Complement_Complement. assumption.
+  + apply Im_def. assumption.
   + assumption.
 - destruct H.
-  red; red; intro.
-  destruct H1.
+  inversion H; subst; clear H.
+  intros ?.
   destruct H.
-  pose proof (H1 _ H).
-  contradiction.
+  firstorder.
 Qed.
 
 Lemma Complement_FamilyUnion: forall F:Family T,
     Complement (FamilyUnion F) =
-    FamilyIntersection [ S:Ensemble T |
-                         In F (Complement S) ].
+    FamilyIntersection (Im F Complement).
 Proof.
 intros.
 apply Extensionality_Ensembles; split; red; intros.
-- constructor. intros.
-  destruct H0.
-  apply NNPP. red; intro.
-  red in H; red in H. contradict H.
-  exists (Complement S); assumption.
-- red; red. intro.
-  destruct H.
-  destruct H0.
-  specialize (H (Complement S)).
-  apply H.
-  2: { assumption. }
-  constructor. rewrite Complement_Complement.
+- constructor. intros S HS.
+  destruct HS as [U HU S]. subst.
+  intros HUx. apply H.
+  exists U; auto.
+- destruct H as [x Hx].
+  intros Hx0.
+  destruct Hx0.
+  specialize (Hx (Complement S)).
+  apply Hx; auto.
+  apply Im_def.
   assumption.
 Qed.