proposition: Lemma homeomorphism_is_invertible: forall {X Y:TopologicalSpace} (f:X -> Y), homeomorphism f -> invertible f.
proof: Proof. intros. destruct H as [g]. exists g; trivial. Qed.
imports: ZornsLemma(EnsemblesTactics Relation_Definitions_Implicit)