theorem Th12: :: WAYBEL24:12

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 monotone & Proj (f,b) is monotone ) ) holds
f is monotone