set L = the 1 -element strict Lattice;
consider x being object such that
A1: the carrier of the 1 -element strict Lattice = {x} by ZFMISC_1:131;
reconsider x = x as Element of the 1 -element strict Lattice by A1, TARSKI:def 1;
reconsider L = the 1 -element strict Lattice as complete Lattice ;
for a being Element of L ex X being Subset of L st
( ( for u being Element of L st u in X holds
u is atomic ) & a = "\/" (X,L) )

proof

let a be Element of L; :: thesis: ex X being Subset of L st
( ( for u being Element of L st u in X holds
u is atomic ) & a = "\/" (X,L) )
for u being object st u in {} holds
u in the carrier of L ;
then A2: ( ( for u being Element of L st u in {} holds
u is atomic ) & {} is Subset of L ) by TARSKI:def 3;
( a = x & x = "\/" ({},L) ) by A1, TARSKI:def 1;
hence ex X being Subset of L st
( ( for u being Element of L st u in X holds
u is atomic ) & a = "\/" (X,L) ) by A2; :: thesis: verum

end;

then L is atomic ;
hence ex b₁ being Lattice st
( b₁ is atomic & b₁ is complete ) ; :: thesis: verum