set f = Fodor_implication ;
a0:
for x1, x2, y being Element of [.0,1.] st x1 <= x2 holds
Fodor_implication . (x1,y) >= Fodor_implication . (x2,y)
b0:
for x, y1, y2 being Element of [.0,1.] st y1 <= y2 holds
Fodor_implication . (x,y1) <= Fodor_implication . (x,y2)
AA:
( 0 in [.0,1.] & 1 in [.0,1.] )
by XXREAL_1:1;
then Fodor_implication . (1,0) =
max ((1 - 1),0)
by Fodor
.=
0
;
hence
( Fodor_implication is decreasing_on_1st & Fodor_implication is increasing_on_2nd & Fodor_implication is 00-dominant & Fodor_implication is 11-dominant & Fodor_implication is 10-weak )
by a0, b0, AA, Fodor; verum