theorem :: WAYBEL_6:29

for L being Boolean LATTICE
for l being Element of L st l <> Top L holds
( l is prime iff for x being Element of L st x > l holds
x = Top L )