let S, T be TopSpace; :: thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) implies Omega S = Omega T )
assume A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) ; :: thesis: Omega S = Omega T
A2: TopStruct(# the carrier of (Omega S), the topology of (Omega S) #) = TopStruct(# the carrier of S, the topology of S #) by Def2
.= TopStruct(# the carrier of (Omega T), the topology of (Omega T) #) by A1, Def2 ;
the InternalRel of (Omega S) = the InternalRel of (Omega T)
proof
let a, b be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [a,b] in the InternalRel of (Omega S) or [a,b] in the InternalRel of (Omega T) ) & ( not [a,b] in the InternalRel of (Omega T) or [a,b] in the InternalRel of (Omega S) ) )
thus ( [a,b] in the InternalRel of (Omega S) implies [a,b] in the InternalRel of (Omega T) ) :: thesis: ( not [a,b] in the InternalRel of (Omega T) or [a,b] in the InternalRel of (Omega S) )
proof
assume A3: [a,b] in the InternalRel of (Omega S) ; :: thesis: [a,b] in the InternalRel of (Omega T)
then reconsider s1 = a, s2 = b as Element of (Omega S) by ZFMISC_1:87;
reconsider t1 = s1, t2 = s2 as Element of (Omega T) by A2;
s1 <= s2 by A3;
then consider Y being Subset of S such that
A4: Y = {s2} and
A5: s1 in Cl Y by Def2;
reconsider Z = Y as Subset of T by A1;
t1 in Cl Z by A1, A5, TOPS_3:80;
then t1 <= t2 by A4, Def2;
hence [a,b] in the InternalRel of (Omega T) ; :: thesis: verum
end;
assume A6: [a,b] in the InternalRel of (Omega T) ; :: thesis: [a,b] in the InternalRel of (Omega S)
then reconsider s1 = a, s2 = b as Element of (Omega T) by ZFMISC_1:87;
reconsider t1 = s1, t2 = s2 as Element of (Omega S) by A2;
s1 <= s2 by A6;
then consider Y being Subset of T such that
A7: Y = {s2} and
A8: s1 in Cl Y by Def2;
reconsider Z = Y as Subset of S by A1;
t1 in Cl Z by A1, A8, TOPS_3:80;
then t1 <= t2 by A7, Def2;
hence [a,b] in the InternalRel of (Omega S) ; :: thesis: verum
end;
hence Omega S = Omega T by A2; :: thesis: verum