let L be complete Boolean LATTICE; :: thesis: for x being Element of L
for A being Subset of L st A c= ATOM L holds
( x in A iff ( x is atom & x <= sup A ) )
let x be Element of L; :: thesis: for A being Subset of L st A c= ATOM L holds
( x in A iff ( x is atom & x <= sup A ) )
let A be Subset of L; :: thesis: ( A c= ATOM L implies ( x in A iff ( x is atom & x <= sup A ) ) )
assume A1: A c= ATOM L ; :: thesis: ( x in A iff ( x is atom & x <= sup A ) )
thus ( x in A implies ( x is atom & x <= sup A ) ) :: thesis: ( x is atom & x <= sup A implies x in A )

proof

assume A2: x in A ; :: thesis: ( x is atom & x <= sup A )
hence x is atom by A1, Def2; :: thesis: x <= sup A
sup A is_>=_than A by YELLOW_0:32;
hence x <= sup A by A2, LATTICE3:def 9; :: thesis: verum

end;

thus ( x is atom & x <= sup A implies x in A ) :: thesis: verum

proof

assume that
A3: x is atom and
A4: x <= sup A and
A5: not x in A ; :: thesis: contradiction

now :: thesis: for b being Element of L st b in { (x "/\" y) where y is Element of L : y in A } holds
b <= Bottom L

let b be Element of L; :: thesis: ( b in { (x "/\" y) where y is Element of L : y in A } implies b <= Bottom L )
assume b in { (x "/\" y) where y is Element of L : y in A } ; :: thesis: b <= Bottom L
then consider y being Element of L such that
A6: b = x "/\" y and
A7: y in A ;
y is atom by A1, A7, Def2;
hence b <= Bottom L by A3, A5, A6, A7, Th24; :: thesis: verum

end;

then A8: Bottom L is_>=_than { (x "/\" y) where y is Element of L : y in A } by LATTICE3:def 9;
x = x "/\" (sup A) by A4, YELLOW_0:25
.= "\/" ( { (x "/\" y) where y is Element of L : y in A } ,L) by Th23 ;
then x <= Bottom L by A8, YELLOW_0:32;
then x = Bottom L by YELLOW_5:19;
hence contradiction by A3; :: thesis: verum

end;