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 ;

thus X c= ATOM L :: thesis: x = sup X

hence x = sup X by A1, A4, YELLOW_0:32; :: thesis: verum

( 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

take
X
; :: thesis: ( X c= ATOM L & x = sup X )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

hence x <= b by A1, A2, YELLOW_0:32; :: thesis: verum

end;assume A5: b is_>=_than X ; :: thesis: x <= b

now :: thesis: for c being Element of L st c in X1 holds

c <= b

then
b is_>=_than X1
by LATTICE3:def 9;c <= b

let c be Element of L; :: thesis: ( c in X1 implies c <= b )

assume A6: c in X1 ; :: thesis: c <= b

end;assume A6: c in X1 ; :: thesis: c <= b

now :: thesis: c <= bend;

hence
c <= b
; :: thesis: verumper cases
( c <> Bottom L or c = Bottom L )
;

end;

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;then c in X by A6, XBOOLE_0:def 5;

hence c <= b by A5, LATTICE3:def 9; :: thesis: verum

hence x <= b by A1, A2, YELLOW_0:32; :: thesis: verum

thus X c= ATOM L :: thesis: x = sup X

proof

A9:
x is_>=_than X1
by A1, A2, YELLOW_0:32;
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;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

now :: thesis: for c being Element of L st c in X holds

c <= x

then
x is_>=_than X
by LATTICE3:def 9;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;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

hence x = sup X by A1, A4, YELLOW_0:32; :: thesis: verum