:: deftheorem defines Ids WAYBEL_0:def 23 :
for L being non empty reflexive transitive RelStr holds Ids L = { X where X is Ideal of L : verum } ;