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
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 ) ) ; :: thesis: R1 = R2
the InternalRel of R1 = the InternalRel of R2

proof

let x, y be object ; :: 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 A6: [x,y] in the InternalRel of R1 ; :: thesis: [x,y] in the InternalRel of R2
then reconsider x1 = x, y1 = y as Element of R1 by ZFMISC_1:87;
reconsider x2 = x, y2 = y as Element of R2 by A2, A4, A6, ZFMISC_1:87;
x1 <= y1 by A6;
then ex Y being Subset of T st
( Y = {y1} & x1 in Cl Y ) by A3;
then x2 <= y2 by A5;
hence [x,y] in the InternalRel of R2 ; :: thesis: verum

end;

assume A7: [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: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 ; :: thesis: verum

end;

hence R1 = R2 by A2, A4; :: thesis: verum