:: deftheorem defines Filt WAYBEL_0:def 24 :
for L being non empty reflexive transitive RelStr holds Filt L = { X where X is Filter of L : verum } ;