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;