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

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