theorem Th11: :: WAYBEL24:11

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