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 set ; :: 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:106;
reconsider t1 = s1, t2 = s2 as Element of (Omega T) by A2;
s1 <= s2 by A3, ORDERS_2:def 9;
then consider Y being Subset of S such that
A4: ( Y = {s2} & s1 in Cl Y ) by Def2;
reconsider Z = Y as Subset of T by A1;
( Z = {t2} & t1 in Cl Z ) by A1, A4, TOPS_3:80;
then t1 <= t2 by Def2;
hence [a,b] in the InternalRel of (Omega T) by ORDERS_2:def 9; :: thesis: verum

end;

assume A5: [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:106;
reconsider t1 = s1, t2 = s2 as Element of (Omega S) by A2;
s1 <= s2 by A5, ORDERS_2:def 9;
then consider Y being Subset of T such that
A6: ( Y = {s2} & s1 in Cl Y ) by Def2;
reconsider Z = Y as Subset of S by A1;
( Z = {t2} & t1 in Cl Z ) by A1, A6, TOPS_3:80;
then t1 <= t2 by Def2;
hence [a,b] in the InternalRel of (Omega S) by ORDERS_2:def 9; :: thesis: verum

end;

hence Omega S = Omega T by A2; :: thesis: verum