theorem Th20: :: WAYBEL_7:20

for L being Boolean LATTICE
for F being Filter of L holds
( F is prime iff for a being Element of L holds
( a in F or 'not' a in F ) )