let S, T be TopStruct ; :: thesis: ( ex f being Function of S,T st f is being_homeomorphism implies ( S is empty iff T is empty ) )
given f being Function of S,T such that A1: f is being_homeomorphism ; :: thesis: ( S is empty iff T is empty )
A2: dom f = [#] S by A1, TOPS_2:def 5;
rng f = [#] T by A1, TOPS_2:def 5;
hence ( S is empty iff T is empty ) by A2, Lm35, Lm36; :: thesis: verum