let L1, L2 be non empty RelStr ; :: thesis: for f being Function of L1,L2 st f is sups-preserving holds
f is join-preserving
let f be Function of L1,L2; :: thesis: ( f is sups-preserving implies f is join-preserving )
assume f is sups-preserving ; :: thesis: f is join-preserving
then for x, y being Element of L1 holds f preserves_sup_of {x,y} by WAYBEL_0:def 33;
hence f is join-preserving by WAYBEL_0:def 35; :: thesis: verum