let L be lower-bounded LATTICE; ( L is meet-continuous implies for x, y being Element of L holds
( x << y iff for I being Ideal of L st y = sup I holds
x in I ) )
assume A1:
( L is up-complete & L is satisfying_MC )
; WAYBEL_2:def 7 for x, y being Element of L holds
( x << y iff for I being Ideal of L st y = sup I holds
x in I )
let x, y be Element of L; ( x << y iff for I being Ideal of L st y = sup I holds
x in I )
hereby ( ( for I being Ideal of L st y = sup I holds
x in I ) implies x << y )
end;
assume A3:
for I being Ideal of L st y = sup I holds
x in I
; x << y
now for I being Ideal of L st y <= sup I holds
x in Ilet I be
Ideal of
L;
( y <= sup I implies x in I )A4:
ex_sup_of finsups ({y} "/\" I),
L
by A1, WAYBEL_0:75;
assume
y <= sup I
;
x in Ithen
y "/\" (sup I) = y
by YELLOW_0:25;
then y =
sup ({y} "/\" I)
by A1
.=
sup (finsups ({y} "/\" I))
by A1, WAYBEL_0:55
.=
sup (downarrow (finsups ({y} "/\" I)))
by A4, WAYBEL_0:33
;
then
x in downarrow (finsups ({y} "/\" I))
by A3;
then consider z being
Element of
L such that A5:
x <= z
and A6:
z in finsups ({y} "/\" I)
by WAYBEL_0:def 15;
consider Y being
finite Subset of
({y} "/\" I) such that A7:
z = "\/" (
Y,
L)
and
ex_sup_of Y,
L
by A6;
set i = the
Element of
I;
reconsider i = the
Element of
I as
Element of
L ;
A8:
ex_sup_of {i},
L
by YELLOW_0:38;
A9:
sup {i} = i
by YELLOW_0:39;
ex_sup_of {} ,
L
by A1, YELLOW_0:17;
then
"\/" (
{},
L)
<= sup {i}
by A8, XBOOLE_1:2, YELLOW_0:34;
then A10:
"\/" (
{},
L)
in I
by A9, WAYBEL_0:def 19;
Y c= I
then
z in I
by A7, A10, WAYBEL_0:42;
hence
x in I
by A5, WAYBEL_0:def 19;
verum end;
hence
x << y
by A1, Th21; verum