:: deftheorem Def2 defines prime WAYBEL_7:def 2 :
for L being with_suprema Poset
for F being Filter of L holds
( F is prime iff for x, y being Element of L holds
( not x "\/" y in F or x in F or y in F ) );