:: deftheorem defines Filt_0 WAYBEL_0:def 26 :
for L being non empty reflexive transitive RelStr holds Filt_0 L = (Filt L) \/ {{}};