:: deftheorem D1 defines "\/"-preserving LATTICE4:def 1 :
for L1, L2 being non empty \/-SemiLattStr
for f being Function of L1,L2 holds
( f is "\/"-preserving iff for a, b being Element of L1 holds f . (a "\/" b) = (f . a) "\/" (f . b) );