let f be Function of S,T; :: thesis: ( f is sups-preserving implies f is finite-sups-preserving )
assume for X being Subset of S holds f preserves_sup_of X ; :: according to WAYBEL_0:def 33 :: thesis: f is finite-sups-preserving
hence for X being finite Subset of S holds f preserves_sup_of X ; :: according to WAYBEL34:def 15 :: thesis: verum