let L be complete LATTICE; :: thesis:
let x be Element of L; :: thesis:
set X = { I where I is Ideal of L : x <= sup I } ;
{ I where I is Ideal of L : x <= sup I } c= bool the carrier of L

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in { I where I is Ideal of L : x <= sup I } ; :: thesis:
then ex I being Ideal of L st
( a = I & x <= sup I ) ;
hence a in bool the carrier of L ; :: thesis:

end;

then reconsider X9 = { I where I is Ideal of L : x <= sup I } as Subset-Family of L ;
sup (downarrow x) = x by WAYBEL_0:34;
then A1: downarrow x in { I where I is Ideal of L : x <= sup I } ;
thus meet { I where I is Ideal of L : x <= sup I } c= waybelow x :: according to XBOOLE_0:def 10 :: thesis:

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume A2: a in meet { I where I is Ideal of L : x <= sup I } ; :: thesis:
then a in meet X9 ;
then reconsider y = a as Element of L ;

let I be Ideal of L; :: thesis:
assume x <= sup I ; :: thesis:
then I in { I where I is Ideal of L : x <= sup I } ;
hence y in I by A2, SETFAM_1:def 1; :: thesis:

end;

end;

thus waybelow x c= meet { I where I is Ideal of L : x <= sup I } :: thesis:

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in waybelow x ; :: thesis:
then a in { y where y is Element of L : y << x } by WAYBEL_3:def 3;
then A3: ex a9 being Element of L st
( a9 = a & a9 << x ) ;
for Y being set st Y in { I where I is Ideal of L : x <= sup I } holds
a in Y

let Y be set ; :: thesis:
assume Y in { I where I is Ideal of L : x <= sup I } ; :: thesis:
then ex I being Ideal of L st
( Y = I & x <= sup I ) ;
hence a in Y by A3, WAYBEL_3:20; :: thesis:

end;

hence a in meet { I where I is Ideal of L : x <= sup I } by A1, SETFAM_1:def 1; :: thesis:

end;