:: deftheorem Def1 defines prime WAYBEL_7:def 1 :
for L being with_infima Poset
for I being Ideal of L holds
( I is prime iff for x, y being Element of L holds
( not x "/\" y in I or x in I or y in I ) );