let R1, R2 be strict TopRelStr ; ( TopStruct(# the carrier of R1, the topology of R1 #) = TopStruct(# the carrier of T, the topology of T #) & ( for x, y being Element of R1 holds
( x <= y iff ex Y being Subset of T st
( Y = {y} & x in Cl Y ) ) ) & TopStruct(# the carrier of R2, the topology of R2 #) = TopStruct(# the carrier of T, the topology of T #) & ( for x, y being Element of R2 holds
( x <= y iff ex Y being Subset of T st
( Y = {y} & x in Cl Y ) ) ) implies R1 = R2 )
assume that
A2:
TopStruct(# the carrier of R1, the topology of R1 #) = TopStruct(# the carrier of T, the topology of T #)
and
A3:
for x, y being Element of R1 holds
( x <= y iff ex Y being Subset of T st
( Y = {y} & x in Cl Y ) )
and
A4:
TopStruct(# the carrier of R2, the topology of R2 #) = TopStruct(# the carrier of T, the topology of T #)
and
A5:
for x, y being Element of R2 holds
( x <= y iff ex Y being Subset of T st
( Y = {y} & x in Cl Y ) )
; R1 = R2
the InternalRel of R1 = the InternalRel of R2
proof
let x,
y be
object ;
RELAT_1:def 2 ( ( not [x,y] in the InternalRel of R1 or [x,y] in the InternalRel of R2 ) & ( not [x,y] in the InternalRel of R2 or [x,y] in the InternalRel of R1 ) )
assume A7:
[x,y] in the
InternalRel of
R2
;
[x,y] in the InternalRel of R1
then reconsider x2 =
x,
y2 =
y as
Element of
R2 by ZFMISC_1:87;
reconsider x1 =
x,
y1 =
y as
Element of
R1 by A2, A4, A7, ZFMISC_1:87;
x2 <= y2
by A7;
then
ex
Y being
Subset of
T st
(
Y = {y2} &
x2 in Cl Y )
by A5;
then
x1 <= y1
by A3;
hence
[x,y] in the
InternalRel of
R1
;
verum
end;
hence
R1 = R2
by A2, A4; verum