:: deftheorem defines principal WAYBEL_0:def 21 :
for L being non empty reflexive transitive RelStr
for I being Ideal of L holds
( I is principal iff ex x being Element of L st
( x in I & x is_>=_than I ) );