let T1, T2 be TopSpace; :: thesis: ( T1,T2 are_homeomorphic iff [#] T1, [#] T2 are_homeomorphic )
A1: ( T1 | ([#] T1) = TopStruct(# the carrier of T1, the topology of T1 #) & T2 | ([#] T2) = TopStruct(# the carrier of T2, the topology of T2 #) ) by TSEP_1:93;

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

suppose A2: not T2 is empty ; :: thesis: ( T1,T2 are_homeomorphic iff [#] T1, [#] T2 are_homeomorphic )

thus ( T1,T2 are_homeomorphic implies [#] T1, [#] T2 are_homeomorphic ) by A1, A2, TOPREALA:15; :: thesis: ( [#] T1, [#] T2 are_homeomorphic implies T1,T2 are_homeomorphic )
assume [#] T1, [#] T2 are_homeomorphic ; :: thesis: T1,T2 are_homeomorphic
then TopStruct(# the carrier of T1, the topology of T1 #), TopStruct(# the carrier of T2, the topology of T2 #) are_homeomorphic by A1;
hence T1,T2 are_homeomorphic by A2, TOPREALA:15; :: thesis: verum

end;

suppose A3: T2 is empty ; :: thesis: ( T1,T2 are_homeomorphic iff [#] T1, [#] T2 are_homeomorphic )

hereby :: thesis: ( [#] T1, [#] T2 are_homeomorphic implies T1,T2 are_homeomorphic )

assume T1,T2 are_homeomorphic ; :: thesis: [#] T1, [#] T2 are_homeomorphic
then ( T1 is empty iff T2 is empty ) by YELLOW14:18;
then T1 | ([#] T1),T2 | ([#] T2) are_homeomorphic by A3, Lm1;
hence [#] T1, [#] T2 are_homeomorphic ; :: thesis: verum

end;

assume [#] T1, [#] T2 are_homeomorphic ; :: thesis: T1,T2 are_homeomorphic
then T1 | ([#] T1),T2 | ([#] T2) are_homeomorphic ;
then T1 is empty by A3, YELLOW14:18;
hence T1,T2 are_homeomorphic by A3, Lm1; :: thesis: verum

end;

end;