theorem :: WAYBEL15:21

for L being Boolean LATTICE holds ATOM L = (PRIME (L opp)) \ {(Bottom L)}