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 )
( rng f = [#] T & dom f = [#] S ) by A1, TOPS_2:def 5;
hence ( S is empty iff T is empty ) by Lm28, Lm29; :: thesis: verum