:: deftheorem defines prime FILTER_2:def 10 :
for L being Lattice
for I being Ideal of L holds
( I is prime iff for p, q being Element of L holds
( p "/\" q in I iff ( p in I or q in I ) ) );