proposition: Lemma option_Full_set_Im (X : Type) : Full_set = Add (Im Full_set (@Some X)) None.
proof: Proof. apply Extensionality_Ensembles; split; red; intros. 2: { constructor. } destruct x. - left. exists x; constructor. - right. constructor. Qed.
imports: ZornsLemma(EnsemblesImplicit) ZornsLemma(FunctionProperties)