theorem Th33: :: MESFUN12:33

for X1, X2 being non empty set
for x being Element of X1
for y being Element of X2
for f being PartFunc of [:X1,X2:],ExtREAL st f is nonpositive holds
( ProjPMap1 (f,x) is nonpositive & ProjPMap2 (f,y) is nonpositive )