theorem Th25: :: WAYBEL15:25

for L being complete Boolean LATTICE
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 ) )