proposition: Lemma empty_family_intersection: FamilyIntersection (@Empty_set (Ensemble T)) = Full_set.
proof: Proof. apply Extensionality_Ensembles. unfold Same_set. unfold Included. intuition. constructor. constructor. intros. contradiction H0. Qed.
imports: Ensembles EnsemblesImplicit