let S, T be non empty RelStr ; :: thesis: for f being Function of S,T st f is finite-sups-preserving holds
( f is join-preserving & f is bottom-preserving )
let f be Function of S,T; :: thesis: ( f is finite-sups-preserving implies ( f is join-preserving & f is bottom-preserving ) )
assume A1: for X being finite Subset of S holds f preserves_sup_of X ; :: according to WAYBEL34:def 15 :: thesis: ( f is join-preserving & f is bottom-preserving )
thus f is join-preserving :: thesis: f is bottom-preserving

proof

let x, y be Element of S; :: according to WAYBEL_0:def 35 :: thesis: f preserves_sup_of {x,y}
thus f preserves_sup_of {x,y} by A1; :: thesis: verum

end;

thus f preserves_sup_of {} S by A1; :: according to WAYBEL34:def 16 :: thesis: verum