theorem Th21: :: WAYBEL_7:21

for X being set
for F being Filter of (BoolePoset X) holds
( F is prime iff for A being Subset of X holds
( A in F or X \ A in F ) )