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;

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 )
;

end;

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;( 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

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;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