let LR1, LR2 be strict complete continuous LATTICE; ( the carrier of LR1 = Class (EqRel R) & ( for x, y being Element of LR1 holds
( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) & the carrier of LR2 = Class (EqRel R) & ( for x, y being Element of LR2 holds
( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) implies LR1 = LR2 )
assume that
A11:
the carrier of LR1 = Class (EqRel R)
and
A12:
for x, y being Element of LR1 holds
( x <= y iff "/\" (x,L) <= "/\" (y,L) )
and
A13:
the carrier of LR2 = Class (EqRel R)
and
A14:
for x, y being Element of LR2 holds
( x <= y iff "/\" (x,L) <= "/\" (y,L) )
; LR1 = LR2
set cLR2 = the carrier of LR2;
set cLR1 = the carrier of LR1;
now for z being set holds
( ( z in the InternalRel of LR1 implies z in the InternalRel of LR2 ) & ( z in the InternalRel of LR2 implies z in the InternalRel of LR1 ) )let z be
set ;
( ( z in the InternalRel of LR1 implies z in the InternalRel of LR2 ) & ( z in the InternalRel of LR2 implies z in the InternalRel of LR1 ) )hereby ( z in the InternalRel of LR2 implies z in the InternalRel of LR1 )
assume A15:
z in the
InternalRel of
LR1
;
z in the InternalRel of LR2then consider x,
y being
set such that A16:
(
x in the
carrier of
LR1 &
y in the
carrier of
LR1 )
and A17:
z = [x,y]
by ZFMISC_1:def 2;
reconsider x =
x,
y =
y as
Element of
LR1 by A16;
reconsider x9 =
x,
y9 =
y as
Element of
LR2 by A11, A13;
x <= y
by A15, A17, ORDERS_2:def 5;
then
"/\" (
x,
L)
<= "/\" (
y,
L)
by A12;
then
x9 <= y9
by A14;
hence
z in the
InternalRel of
LR2
by A17, ORDERS_2:def 5;
verum
end; assume A18:
z in the
InternalRel of
LR2
;
z in the InternalRel of LR1then consider x,
y being
set such that A19:
(
x in the
carrier of
LR2 &
y in the
carrier of
LR2 )
and A20:
z = [x,y]
by ZFMISC_1:def 2;
reconsider x =
x,
y =
y as
Element of
LR2 by A19;
reconsider x9 =
x,
y9 =
y as
Element of
LR1 by A11, A13;
x <= y
by A18, A20, ORDERS_2:def 5;
then
"/\" (
x,
L)
<= "/\" (
y,
L)
by A14;
then
x9 <= y9
by A12;
hence
z in the
InternalRel of
LR1
by A20, ORDERS_2:def 5;
verum end;
hence
LR1 = LR2
by A11, A13, TARSKI:1; verum