proposition: Lemma empty_family_union: FamilyUnion (@Empty_set (Ensemble T)) = Empty_set.
proof: Proof. apply Extensionality_Ensembles. unfold Same_set. unfold Included. intuition. destruct H. contradiction H. contradiction H. Qed.
imports: Ensembles EnsemblesImplicit