:: deftheorem Def2 defines filtered WAYBEL_0:def 2 :
for L being RelStr
for X being Subset of L holds
( X is filtered iff for x, y being Element of L st x in X & y in X holds
ex z being Element of L st
( z in X & z <= x & z <= y ) );