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 set ; :: 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 consider I being Ideal of L such that
A1: ( a = I & x <= sup I ) ;
thus a in bool the carrier of L by A1; :: thesis: verum

end;

then reconsider X' = { I where I is Ideal of L : x <= sup I } as Subset-Family of L ;
sup (downarrow x) = x by WAYBEL_0:34;
then A2: 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 set ; :: 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 A3: a in meet { I where I is Ideal of L : x <= sup I } ; :: thesis: a in waybelow x
then a in meet X' ;
then reconsider y = a as Element of L ;

now

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 A3, 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 set ; :: 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 consider a' being Element of L such that
A4: ( a' = a & a' << 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 consider I being Ideal of L such that
A5: ( Y = I & x <= sup I ) ;
thus a in Y by A4, A5, WAYBEL_3:20; :: thesis: verum

end;

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

end;