let T1, T2, T3 be TopSpace; 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; 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; 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; ( A1,A2 are_homeomorphic & A2,A3 are_homeomorphic implies A1,A3 are_homeomorphic )
assume A1:
A1,A2 are_homeomorphic
; ( 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
; 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
;
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;
verum end; end;