let L be Boolean LATTICE; :: thesis: ( L is completely-distributive implies ( L is complete & ( for x being Element of L ex X being Subset of L st
( X c= ATOM L & x = sup X ) ) ) )

assume A1: L is completely-distributive ; :: thesis: ( L is complete & ( for x being Element of L ex X being Subset of L st
( X c= ATOM L & x = sup X ) ) )

hence L is complete ; :: thesis: for x being Element of L ex X being Subset of L st
( X c= ATOM L & x = sup X )

let x be Element of L; :: thesis: ex X being Subset of L st
( X c= ATOM L & x = sup X )

consider X1 being Subset of L such that
A2: x = sup X1 and
A3: for y being Element of L st y in X1 holds
y is co-prime by ;
reconsider X = X1 \ {()} as Subset of L ;
A4: now :: thesis: for b being Element of L st b is_>=_than X holds
x <= b
let b be Element of L; :: thesis: ( b is_>=_than X implies x <= b )
assume A5: b is_>=_than X ; :: thesis: x <= b
now :: thesis: for c being Element of L st c in X1 holds
c <= b
let c be Element of L; :: thesis: ( c in X1 implies c <= b )
assume A6: c in X1 ; :: thesis: c <= b
hence c <= b ; :: thesis: verum
end;
then b is_>=_than X1 by LATTICE3:def 9;
hence x <= b by ; :: thesis: verum
end;
take X ; :: thesis: ( X c= ATOM L & x = sup X )
thus X c= ATOM L :: thesis: x = sup X
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in X or z in ATOM L )
assume A7: z in X ; :: thesis: z in ATOM L
then reconsider z9 = z as Element of L ;
not z in {()} by ;
then A8: z9 <> Bottom L by TARSKI:def 1;
z in X1 by ;
then z9 is co-prime by A3;
then z9 is atom by ;
hence z in ATOM L by Def2; :: thesis: verum
end;
A9: x is_>=_than X1 by ;
now :: thesis: for c being Element of L st c in X holds
c <= x
let c be Element of L; :: thesis: ( c in X implies c <= x )
assume c in X ; :: thesis: c <= x
then c in X1 by XBOOLE_0:def 5;
hence c <= x by ; :: thesis: verum
end;
then x is_>=_than X by LATTICE3:def 9;
hence x = sup X by ; :: thesis: verum