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));
A1: H1( BooleLatt X) = bool X by Def1;
reconsider p = union (x /\ (bool X)) as Element of (BooleLatt X) by 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 A1, XBOOLE_0:def 4;
then q c= p by ZFMISC_1:74;
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 A2: for q being Element of (BooleLatt X) st q in x holds
q [= r ; :: according to LATTICE3:def 17 :: thesis: p [= r
now :: thesis: for z being set st z in x /\ (bool X) holds
z c= r
let z be set ; :: thesis: ( z in x /\ (bool X) implies z c= r )
assume A3: z in x /\ (bool X) ; :: thesis: z c= r
then A4: z in x by XBOOLE_0:def 4;
reconsider z9 = z as Element of (BooleLatt X) by A1, A3;
z9 [= r by A2, A4;
hence z c= r by Th2; :: thesis: verum
end;
then p c= r by ZFMISC_1:76;
hence p [= r by Th2; :: thesis: verum