:: deftheorem defines finite-sups-preserving WAYBEL34:def 15 :
for S, T being non empty RelStr
for f being Function of S,T holds
( f is finite-sups-preserving iff for X being finite Subset of S holds f preserves_sup_of X );