let T1, T2, T3 be TopSpace; :: thesis: for A1 being Subset of T1
for A2 being Subset of T2
for A3 being Subset of T3 st A1,A2 are_homeomorphic & A2,A3 are_homeomorphic holds
A1,A3 are_homeomorphic
let A1 be Subset of T1; :: thesis: for A2 being Subset of T2
for A3 being Subset of T3 st A1,A2 are_homeomorphic & A2,A3 are_homeomorphic holds
A1,A3 are_homeomorphic
let A2 be Subset of T2; :: thesis: for A3 being Subset of T3 st A1,A2 are_homeomorphic & A2,A3 are_homeomorphic holds
A1,A3 are_homeomorphic
let A3 be Subset of T3; :: thesis: ( A1,A2 are_homeomorphic & A2,A3 are_homeomorphic implies A1,A3 are_homeomorphic )
assume A1: A1,A2 are_homeomorphic ; :: thesis: ( not A2,A3 are_homeomorphic or A1,A3 are_homeomorphic )
then A2: T1 | A1,T2 | A2 are_homeomorphic by METRIZTS:def 1;
assume A3: A2,A3 are_homeomorphic ; :: thesis: A1,A3 are_homeomorphic
then A4: T2 | A2,T3 | A3 are_homeomorphic by METRIZTS:def 1;

per cases ( not A2 is empty or A2 is empty ) ;

suppose A5: not A2 is empty ; :: thesis: A1,A3 are_homeomorphic

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: verum

end;

suppose A2 is empty ; :: thesis: A1,A3 are_homeomorphic

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: verum

end;

end;