let T1, T2 be TopSpace; :: thesis: for A1 being Subset of T1
for A2 being Subset of T2 st A1,A2 are_homeomorphic holds
( A1 is empty iff A2 is empty )
let A1 be Subset of T1; :: thesis: for A2 being Subset of T2 st A1,A2 are_homeomorphic holds
( A1 is empty iff A2 is empty )
let A2 be Subset of T2; :: thesis: ( A1,A2 are_homeomorphic implies ( A1 is empty iff A2 is empty ) )
assume A1,A2 are_homeomorphic ; :: thesis: ( A1 is empty iff A2 is empty )
then consider f being Function of (T1 | A1),(T2 | A2) such that
A1: f is being_homeomorphism by METRIZTS:def 1, T_0TOPSP:def 1;
( dom f = [#] (T1 | A1) & rng f = [#] (T2 | A2) & f is one-to-one & f is continuous & f " is continuous ) by A1, TOPS_2:def 5;
hence ( A1 is empty iff A2 is empty ) by PRE_TOPC:def 5; :: thesis: verum