let X be set ; :: thesis: BooleLatt X is complete
set B = BooleLatt X;
let x be set ; :: according to LATTICE3:def 18 :: thesis: ex p being Element of (BooleLatt X) st
( x is_less_than p & ( for r being Element of (BooleLatt X) st x is_less_than r holds
p [= r ) )
set p = union (x /\ (bool X));
x /\ (bool X) c= bool X by XBOOLE_1:17;
then A1: ( union (x /\ (bool X)) c= union (bool X) & union (bool X) = X ) by ZFMISC_1:95, ZFMISC_1:99;
then A2: ( union (x /\ (bool X)) in bool X & H₁( BooleLatt X) = bool X ) by Def1;
reconsider p = union (x /\ (bool X)) as Element of (BooleLatt X) by A1, Def1;
take p ; :: thesis: ( x is_less_than p & ( for r being Element of (BooleLatt X) st x is_less_than r holds
p [= r ) )
thus x is_less_than p :: thesis: for r being Element of (BooleLatt X) st x is_less_than r holds
p [= r

proof

let q be Element of (BooleLatt X); :: according to LATTICE3:def 17 :: thesis: ( q in x implies q [= p )
assume q in x ; :: thesis: q [= p
then q in x /\ (bool X) by A2, XBOOLE_0:def 4;
then q c= p by ZFMISC_1:92;
hence q [= p by Th2; :: thesis: verum

end;

let r be Element of (BooleLatt X); :: thesis: ( x is_less_than r implies p [= r )
assume A3: for q being Element of (BooleLatt X) st q in x holds
q [= r ; :: according to LATTICE3:def 17 :: thesis: p [= r

now

let z be set ; :: thesis: ( z in x /\ (bool X) implies z c= r )
assume A4: z in x /\ (bool X) ; :: thesis: z c= r
then A5: ( z in x & z in bool X ) by XBOOLE_0:def 4;
reconsider z' = z as Element of (BooleLatt X) by A2, A4, XBOOLE_0:def 4;
z' [= r by A3, A5;
hence z c= r by Th2; :: thesis: verum

end;

then p c= r by ZFMISC_1:94;
hence p [= r by Th2; :: thesis: verum