let T1, T2, T3 be TopSpace; :: thesis:
let A1 be Subset of T1; :: thesis:
let A2 be Subset of T2; :: thesis:
let A3 be Subset of T3; :: thesis:
assume A1: A1,A2 are_homeomorphic ; :: thesis:
then A2: T1 | A1,T2 | A2 are_homeomorphic by METRIZTS:def 1;
assume A3: A2,A3 are_homeomorphic ; :: thesis:
then A4: T2 | A2,T3 | A3 are_homeomorphic by METRIZTS:def 1;

suppose A5: not A2 is empty ; :: thesis:

then A6: ( not A1 is empty & not A3 is empty ) by A1, A3, Th7;
( not T1 is empty & not T2 is empty & not T3 is empty ) by A5, A1, A3, Th7;
hence A1,A3 are_homeomorphic by A2, A4, A6, A5, BORSUK_3:3, METRIZTS:def 1; :: thesis:

end;

suppose A2 is empty ; :: thesis:

then A7: ( A1 is empty & A3 is empty ) by A1, A3, Th7;
reconsider f = {} as Function ;
A8: ( the carrier of (T1 | A1) = {} & the carrier of (T3 | A3) = {} ) by A7;
( dom f = {} & rng f = {} ) ;
then reconsider f = f as Function of (T1 | A1),(T3 | A3) by A8, FUNCT_2:1;
A9: ( dom f = [#] (T1 | A1) & rng f = [#] (T3 | A3) ) by A8;
for P1 being Subset of (T3 | A3) st P1 is closed holds
f " P1 is closed ;
then A10: f is continuous by PRE_TOPC:def 6;
reconsider g = f as one-to-one onto PartFunc of {},{} by FUNCTOR0:1;
for P1 being Subset of (T1 | A1) st P1 is closed holds
(f ") " P1 is closed by A7;
then f " is continuous by PRE_TOPC:def 6;
then f is being_homeomorphism by A9, A10, TOPS_2:def 5;
hence A1,A3 are_homeomorphic by METRIZTS:def 1, T_0TOPSP:def 1; :: thesis:

end;

end;