now :: thesis: for x being object holds (~ f) . x <= 0.

let x be object ; :: thesis: (~ f) . b₁ <= 0.

per cases ( not x in dom (~ f) or x in dom (~ f) ) ;

suppose not x in dom (~ f) ; :: thesis: (~ f) . b₁ <= 0.

hence (~ f) . x <= 0. by FUNCT_1:def 2; :: thesis: verum

end;

suppose x in dom (~ f) ; :: thesis: (~ f) . b₁ <= 0.

then consider b, a being object such that
A1: ( b in B & a in A & x = [b,a] ) by ZFMISC_1:def 2;
reconsider a = a as Element of A by A1;
reconsider b = b as Element of B by A1;
f . (a,b) <= 0 by MESFUNC5:8;
then (~ f) . (b,a) <= 0 by FUNCT_4:def 8;
hence (~ f) . x <= 0. by A1; :: thesis: verum

end;

end;

end;

hence ~ f is nonpositive by MESFUNC5:8; :: thesis: verum