theorem :: WAYBEL24:13

for R, S, T being LATTICE
for f being Function of [:R,S:],T st ( for a being Element of R
for b being Element of S holds
( Proj (f,a) is antitone & Proj (f,b) is antitone ) ) holds
f is antitone