let S, T be TopStruct ; :: thesis: ( ( S,T are_homeomorphic or ex f being Function of S,T st
( dom f = [#] S & rng f = [#] T ) ) implies ( S is empty iff T is empty ) )
assume A1: ( S,T are_homeomorphic or ex f being Function of S,T st
( dom f = [#] S & rng f = [#] T ) ) ; :: thesis: ( S is empty iff T is empty )

per cases ( S,T are_homeomorphic or ex f being Function of S,T st
( dom f = [#] S & rng f = [#] T ) ) by A1;

suppose S,T are_homeomorphic ; :: thesis: ( S is empty iff T is empty )

then consider f being Function of S,T such that
A2: f is being_homeomorphism ;
( rng f = [#] T & dom f = [#] S ) by A2;
hence ( S is empty iff T is empty ) ; :: thesis: verum

end;

suppose ex f being Function of S,T st
( dom f = [#] S & rng f = [#] T ) ; :: thesis: ( S is empty iff T is empty )

hence ( S is empty iff T is empty ) ; :: thesis: verum

end;

end;