let L be complete LATTICE; :: thesis: for x being Element of L holds meet { I where I is Ideal of L : x <= sup I } = waybelow x
let x be Element of L; :: thesis: meet { I where I is Ideal of L : x <= sup I } = waybelow x
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

proof

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

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: waybelow x c= meet { I where I is Ideal of L : x <= sup I }

proof

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

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

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

end;

then y << x by WAYBEL_3:21;
hence a in waybelow x by WAYBEL_3:7; :: thesis: verum

end;

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

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in waybelow x or a in meet { I where I is Ideal of L : x <= sup I } )
assume a in waybelow x ; :: thesis: a in meet { I where I is Ideal of L : x <= sup I }
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

proof

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

end;

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

end;