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 )
then A2: L is lower-bounded up-complete LATTICE ;
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 A3: 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 A3, Def1;
hence x in I by WAYBEL_0:def 19; :: thesis: verum

end;

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

now

let I be Ideal of L; :: thesis: ( y <= sup I implies x in I )
A5: 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, WAYBEL_2:def 6
.= sup (finsups ({y} "/\" I)) by A2, WAYBEL_0:55
.= sup (downarrow (finsups ({y} "/\" I))) by A5, WAYBEL_0:33 ;
then x in downarrow (finsups ({y} "/\" I)) by A4;
then consider z being Element of L such that
A6: ( x <= z & z in finsups ({y} "/\" I) ) by WAYBEL_0:def 15;
consider Y being finite Subset of ({y} "/\" I) such that
A7: ( z = "\/" Y,L & ex_sup_of Y,L ) by A6;
consider i being Element of I;
reconsider i = i as Element of L ;
A8: ( ex_sup_of {i},L & sup {i} = i & {} c= {i} ) by XBOOLE_1:2, YELLOW_0:38, YELLOW_0:39;
ex_sup_of {} ,L by A2, YELLOW_0:17;
then "\/" {} ,L <= sup {i} by A8, YELLOW_0:34;
then A9: "\/" {} ,L in I by A8, WAYBEL_0:def 19;
Y c= I

proof

let a be set ; :: 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
A10: ( a = y "/\" j & j in I ) ;
y "/\" j <= j by YELLOW_0:23;
hence a in I by A10, WAYBEL_0:def 19; :: thesis: verum

end;

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

end;

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