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 A1, WAYBEL_6:38;
reconsider X = X1 \ {(Bottom L)} 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

now :: thesis: c <= b

per cases ( c <> Bottom L or c = Bottom L ) ;

suppose c <> Bottom L ; :: thesis: c <= b

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

end;

suppose c = Bottom L ; :: thesis: c <= b

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

end;

end;

end;

hence c <= b ; :: thesis: verum

end;

then b is_>=_than X1 by LATTICE3:def 9;
hence x <= b by A1, A2, YELLOW_0:32; :: 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 {(Bottom L)} by A7, XBOOLE_0:def 5;
then A8: z9 <> Bottom L by TARSKI:def 1;
z in X1 by A7, XBOOLE_0:def 5;
then z9 is co-prime by A3;
then z9 is atom by A8, Th20;
hence z in ATOM L by Def2; :: thesis: verum

end;

A9: x is_>=_than X1 by A1, A2, YELLOW_0:32;

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 A9, LATTICE3:def 9; :: thesis: verum

end;

then x is_>=_than X by LATTICE3:def 9;
hence x = sup X by A1, A4, YELLOW_0:32; :: thesis: verum