let X1, X2 be TopStruct ; :: thesis: ( the carrier of X1 = the carrier of X2 & ( for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
( C1 is open iff C2 is open ) ) implies TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) )
assume A1: the carrier of X1 = the carrier of X2 ; :: thesis: ( ex C1 being Subset of X1 ex C2 being Subset of X2 st
( C1 = C2 & not ( C1 is open iff C2 is open ) ) or TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) )
assume A2: for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
( C1 is open iff C2 is open ) ; :: thesis: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
now :: thesis: for D being object st D in the topology of X2 holds
D in the topology of X1
let D be object ; :: thesis: ( D in the topology of X2 implies D in the topology of X1 )
assume A3: D in the topology of X2 ; :: thesis: D in the topology of X1
then reconsider C2 = D as Subset of X2 ;
reconsider C1 = C2 as Subset of X1 by A1;
C2 is open by A3;
then C1 is open by A2;
hence D in the topology of X1 ; :: thesis: verum
end;
then A4: the topology of X2 c= the topology of X1 by TARSKI:def 3;
now :: thesis: for D being object st D in the topology of X1 holds
D in the topology of X2
let D be object ; :: thesis: ( D in the topology of X1 implies D in the topology of X2 )
assume A5: D in the topology of X1 ; :: thesis: D in the topology of X2
then reconsider C1 = D as Subset of X1 ;
reconsider C2 = C1 as Subset of X2 by A1;
C1 is open by A5;
then C2 is open by A2;
hence D in the topology of X2 ; :: thesis: verum
end;
then the topology of X1 c= the topology of X2 by TARSKI:def 3;
hence TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) by A1, A4, XBOOLE_0:def 10; :: thesis: verum