consider L being non empty trivial strict Lattice;
consider x being set such that
A1: the carrier of L = {x} by REALSET1:def 4;
reconsider x = x as Element of L by A1, TARSKI:def 1;
reconsider L = L 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 )
A2: a = x by A1, TARSKI:def 1;
A3: x = "\/" {} ,L by A1, TARSKI:def 1;
A4: for u being Element of L st u in {} holds
u is atomic ;
for u being set st u in {} holds
u in the carrier of L ;
then {} is Subset of L by TARSKI:def 3;
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, A3, A4; :: thesis: verum

end;

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