proposition: Lemma empty_indexed_intersection: forall {T:Type} (F:IndexedFamily False T), IndexedIntersection F = Full_set.
proof: Proof. intros. apply Extensionality_Ensembles; red; split; red; intros; auto with sets. constructor. destruct a. Qed.
imports: ZornsLemma(EnsemblesImplicit FunctionProperties)