let LR1, LR2 be strict complete continuous LATTICE; :: thesis: ( 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
A10:
the carrier of LR1 = Class (EqRel R)
and
A11:
for x, y being Element of LR1 holds
( x <= y iff "/\" x,L <= "/\" y,L )
and
A12:
the carrier of LR2 = Class (EqRel R)
and
A13:
for x, y being Element of LR2 holds
( x <= y iff "/\" x,L <= "/\" y,L )
; :: thesis: LR1 = LR2
set cLR1 = the carrier of LR1;
set cLR2 = the carrier of LR2;
now let z be
set ;
:: thesis: ( ( 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 :: thesis: ( z in the InternalRel of LR2 implies z in the InternalRel of LR1 )
assume A14:
z in the
InternalRel of
LR1
;
:: thesis: z in the InternalRel of LR2then consider x,
y being
set such that A15:
(
x in the
carrier of
LR1 &
y in the
carrier of
LR1 &
z = [x,y] )
by ZFMISC_1:def 2;
reconsider x =
x,
y =
y as
Element of
LR1 by A15;
reconsider x' =
x,
y' =
y as
Element of
LR2 by A10, A12;
x <= y
by A14, A15, ORDERS_2:def 9;
then
"/\" x,
L <= "/\" y,
L
by A11;
then
x' <= y'
by A13;
hence
z in the
InternalRel of
LR2
by A15, ORDERS_2:def 9;
:: thesis: verum
end; assume A16:
z in the
InternalRel of
LR2
;
:: thesis: z in the InternalRel of LR1then consider x,
y being
set such that A17:
(
x in the
carrier of
LR2 &
y in the
carrier of
LR2 &
z = [x,y] )
by ZFMISC_1:def 2;
reconsider x =
x,
y =
y as
Element of
LR2 by A17;
reconsider x' =
x,
y' =
y as
Element of
LR1 by A10, A12;
x <= y
by A16, A17, ORDERS_2:def 9;
then
"/\" x,
L <= "/\" y,
L
by A13;
then
x' <= y'
by A11;
hence
z in the
InternalRel of
LR1
by A17, ORDERS_2:def 9;
:: thesis: verum end;
hence
LR1 = LR2
by A10, A12, TARSKI:2; :: thesis: verum