let R1, R2 be strict TopRelStr ; :: thesis: ( 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
A3:
TopStruct(# the carrier of R1,the topology of R1 #) = TopStruct(# the carrier of T,the topology of T #)
and
A4:
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
A5:
TopStruct(# the carrier of R2,the topology of R2 #) = TopStruct(# the carrier of T,the topology of T #)
and
A6:
for x, y being Element of R2 holds
( x <= y iff ex Y being Subset of T st
( Y = {y} & x in Cl Y ) )
; :: thesis: R1 = R2
the InternalRel of R1 = the InternalRel of R2
proof
let x,
y be
set ;
:: according to RELAT_1:def 2 :: thesis: ( ( 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 ) )
hereby :: thesis: ( not [x,y] in the InternalRel of R2 or [x,y] in the InternalRel of R1 )
assume A7:
[x,y] in the
InternalRel of
R1
;
:: thesis: [x,y] in the InternalRel of R2then reconsider x1 =
x,
y1 =
y as
Element of
R1 by ZFMISC_1:106;
reconsider x2 =
x,
y2 =
y as
Element of
R2 by A3, A5, A7, ZFMISC_1:106;
x1 <= y1
by A7, ORDERS_2:def 9;
then consider Y being
Subset of
T such that A8:
(
Y = {y1} &
x1 in Cl Y )
by A4;
x2 <= y2
by A6, A8;
hence
[x,y] in the
InternalRel of
R2
by ORDERS_2:def 9;
:: thesis: verum
end;
assume A9:
[x,y] in the
InternalRel of
R2
;
:: thesis: [x,y] in the InternalRel of R1
then reconsider x2 =
x,
y2 =
y as
Element of
R2 by ZFMISC_1:106;
reconsider x1 =
x,
y1 =
y as
Element of
R1 by A3, A5, A9, ZFMISC_1:106;
x2 <= y2
by A9, ORDERS_2:def 9;
then consider Y being
Subset of
T such that A10:
(
Y = {y2} &
x2 in Cl Y )
by A6;
x1 <= y1
by A4, A10;
hence
[x,y] in the
InternalRel of
R1
by ORDERS_2:def 9;
:: thesis: verum
end;
hence
R1 = R2
by A3, A5; :: thesis: verum