let L be lower-bounded LATTICE; :: thesis:
assume A1: ( L is up-complete & L is satisfying_MC ) ; :: according to WAYBEL_2:def 7 :: thesis:
let x, y be Element of L; :: thesis:

hereby :: thesis:

assume A2: x << y ; :: thesis:
let I be Ideal of L; :: thesis:
assume y = sup I ; :: thesis:
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:

end;

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

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

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in Y ; :: thesis:
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:

end;

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

end;

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