let L be lower-bounded LATTICE; :: thesis: ( 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 ) ; :: according to WAYBEL_2:def 7 :: thesis: 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; :: thesis: ( x << y iff for I being Ideal of L st y = sup I holds
x in I )

hereby :: thesis: ( ( for I being Ideal of L st y = sup I holds
x in I ) implies x << y )

assume A2: x << y ; :: thesis: for I being Ideal of L st y = sup I holds
x in I
let I be Ideal of L; :: thesis: ( y = sup I implies x in I )
assume y = sup I ; :: thesis: x in I
then ex d being Element of L st
( d in I & x <= d ) by A2;
hence x in I by WAYBEL_0:def 19; :: thesis: verum

end;

assume A3: for I being Ideal of L st y = sup I holds
x in I ; :: thesis: x << y

now :: thesis: for I being Ideal of L st y <= sup I holds
x in I

let I be Ideal of L; :: thesis: ( y <= sup I implies x in I )
A4: ex_sup_of finsups ({y} "/\" I),L by A1, WAYBEL_0:75;
assume y <= sup I ; :: thesis: x in I
then 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

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Y or a in I )
assume a in Y ; :: thesis: a in I
then a in {y} "/\" I ;
then a in { (y "/\" j) where j is Element of L : j in I } by YELLOW_4:42;
then consider j being Element of L such that
A11: a = y "/\" j and
A12: j in I ;
y "/\" j <= j by YELLOW_0:23;
hence a in I by A11, A12, WAYBEL_0:def 19; :: thesis: verum

end;

then z in I by A7, A10, WAYBEL_0:42;
hence x in I by A5, WAYBEL_0:def 19; :: thesis: verum

end;

hence x << y by A1, Th21; :: thesis: verum