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
A12:
the carrier of LR1 = Class (EqRel R)
and
A13:
for x, y being Element of LR1 holds
( x <= y iff "/\" (x,L) <= "/\" (y,L) )
and
A14:
the carrier of LR2 = Class (EqRel R)
and
A15:
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 object 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
object ;
( ( 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 A16:
z in the
InternalRel of
LR1
;
z in the InternalRel of LR2then consider x,
y being
object such that A17:
(
x in the
carrier of
LR1 &
y in the
carrier of
LR1 )
and A18:
z = [x,y]
by ZFMISC_1:def 2;
reconsider x =
x,
y =
y as
Element of
LR1 by A17;
reconsider x9 =
x,
y9 =
y as
Element of
LR2 by A12, A14;
x <= y
by A16, A18, ORDERS_2:def 5;
then
"/\" (
x,
L)
<= "/\" (
y,
L)
by A13;
then
x9 <= y9
by A15;
hence
z in the
InternalRel of
LR2
by A18, ORDERS_2:def 5;
verum
end; assume A19:
z in the
InternalRel of
LR2
;
z in the InternalRel of LR1then consider x,
y being
object such that A20:
(
x in the
carrier of
LR2 &
y in the
carrier of
LR2 )
and A21:
z = [x,y]
by ZFMISC_1:def 2;
reconsider x =
x,
y =
y as
Element of
LR2 by A20;
reconsider x9 =
x,
y9 =
y as
Element of
LR1 by A12, A14;
x <= y
by A19, A21, ORDERS_2:def 5;
then
"/\" (
x,
L)
<= "/\" (
y,
L)
by A15;
then
x9 <= y9
by A13;
hence
z in the
InternalRel of
LR1
by A21, ORDERS_2:def 5;
verum end;
hence
LR1 = LR2
by A12, A14, TARSKI:2; verum