theorem :: WAYBEL_7:18

for L being with_infima Poset
for I being Ideal of L holds
( I is prime iff ( I ` is Filter of L or I ` = {} ) )