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 closed iff C2 is closed ) ) 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 closed iff C2 is closed ) ) 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 closed iff C2 is closed ) ; :: thesis: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
now :: thesis: for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
( ( C1 is open implies C2 is open ) & ( C2 is open implies C1 is open ) )
let C1 be Subset of X1; :: thesis: for C2 being Subset of X2 st C1 = C2 holds
( ( C1 is open implies C2 is open ) & ( C2 is open implies C1 is open ) )
let C2 be Subset of X2; :: thesis: ( C1 = C2 implies ( ( C1 is open implies C2 is open ) & ( C2 is open implies C1 is open ) ) )
assume A3: C1 = C2 ; :: thesis: ( ( C1 is open implies C2 is open ) & ( C2 is open implies C1 is open ) )
thus ( C1 is open implies C2 is open ) :: thesis: ( C2 is open implies C1 is open )
proof
assume C1 is open ; :: thesis: C2 is open
then C1 ` is closed by TOPS_1:4;
then C2 ` is closed by A1, A2, A3;
hence C2 is open by TOPS_1:4; :: thesis: verum
end;
thus ( C2 is open implies C1 is open ) :: thesis: verum
proof
assume C2 is open ; :: thesis: C1 is open
then C2 ` is closed by TOPS_1:4;
then C1 ` is closed by A1, A2, A3;
hence C1 is open by TOPS_1:4; :: thesis: verum
end;
end;
hence TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) by A1, Th72; :: thesis: verum