for L being non empty transitive RelStr
for X being Subset of L holds
( ( not X is empty & X is filtered ) iff for Y being finite Subset of X ex x being Element of L st
( x in X & x is_<=_than Y ) )