let L be Boolean LATTICE; :: thesis:
assume Z: L is completely-distributive ; :: thesis:
hence L is complete ; :: thesis:
let x be Element of L; :: thesis:
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 Z, WAYBEL_6:38;
reconsider X = X1 \ {(Bottom L)} as Subset of L ;
take X ; :: thesis:
thus X c= ATOM L :: thesis:

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume A4: z in X ; :: thesis:
then A5: ( z in X1 & not z in {(Bottom L)} ) by XBOOLE_0:def 5;
reconsider z' = z as Element of L by A4;
A6: z' <> Bottom L by A5, TARSKI:def 1;
z' is co-prime by A3, A5;
then z' is atom by A6, Th23;
hence z in ATOM L by Def2; :: thesis:

end;

A7: ( x is_>=_than X1 & ( for b being Element of L st b is_>=_than X1 holds
x <= b ) ) by Z, A2, YELLOW_0:32;

now

let c be Element of L; :: thesis:
assume c in X ; :: thesis:
then c in X1 by XBOOLE_0:def 5;
hence c <= x by A7, LATTICE3:def 9; :: thesis:

end;

then A8: x is_>=_than X by LATTICE3:def 9;

now

let b be Element of L; :: thesis:
assume A9: b is_>=_than X ; :: thesis:

now

let c be Element of L; :: thesis:
assume A10: c in X1 ; :: thesis:

now

per cases ;

suppose c <> Bottom L ; :: thesis:

then not c in {(Bottom L)} by TARSKI:def 1;
then c in X by A10, XBOOLE_0:def 5;
hence c <= b by A9, LATTICE3:def 9; :: thesis:

end;

suppose c = Bottom L ; :: thesis:

hence c <= b by YELLOW_0:44; :: thesis:

end;

end;

end;

hence c <= b ; :: thesis:

end;

then b is_>=_than X1 by LATTICE3:def 9;
hence x <= b by Z, A2, YELLOW_0:32; :: thesis:

end;

hence x = sup X by Z, A8, YELLOW_0:32; :: thesis: