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)

proof

let x1, x2, y be Element of [.0,1.]; :: thesis: ( x1 <= x2 implies Fodor_implication . (x1,y) >= Fodor_implication . (x2,y) )
assume Z0: x1 <= x2 ; :: thesis: Fodor_implication . (x1,y) >= Fodor_implication . (x2,y)

per cases ( x2 <= y or x2 > y ) ;

suppose U1: x2 <= y ; :: thesis: Fodor_implication . (x1,y) >= Fodor_implication . (x2,y)

then x1 <= y by Z0, XXREAL_0:2;
then ( Fodor_implication . (x1,y) = 1 & Fodor_implication . (x2,y) = 1 ) by Fodor, U1;
hence Fodor_implication . (x1,y) >= Fodor_implication . (x2,y) ; :: thesis: verum

end;

suppose x2 > y ; :: thesis: Fodor_implication . (x1,y) >= Fodor_implication . (x2,y)

then U2: Fodor_implication . (x2,y) = max ((1 - x2),y) by Fodor;

per cases ( x1 > y or x1 <= y ) ;

suppose x1 > y ; :: thesis: Fodor_implication . (x1,y) >= Fodor_implication . (x2,y)

then U3: Fodor_implication . (x1,y) = max ((1 - x1),y) by Fodor;
- x1 >= - x2 by Z0, XREAL_1:24;
then 1 + (- x1) >= 1 + (- x2) by XREAL_1:7;
hence Fodor_implication . (x1,y) >= Fodor_implication . (x2,y) by U2, XXREAL_0:26, U3; :: thesis: verum

end;

suppose x1 <= y ; :: thesis: Fodor_implication . (x1,y) >= Fodor_implication . (x2,y)

then Fodor_implication . (x1,y) = 1 by Fodor;
hence Fodor_implication . (x1,y) >= Fodor_implication . (x2,y) by XXREAL_1:1; :: thesis: verum

end;

end;

end;

end;

end;

b0: for x, y1, y2 being Element of [.0,1.] st y1 <= y2 holds
Fodor_implication . (x,y1) <= Fodor_implication . (x,y2)

proof

let x, y1, y2 be Element of [.0,1.]; :: thesis: ( y1 <= y2 implies Fodor_implication . (x,y1) <= Fodor_implication . (x,y2) )
assume Z2: y1 <= y2 ; :: thesis: Fodor_implication . (x,y1) <= Fodor_implication . (x,y2)

per cases ( x <= y1 or x > y1 ) ;

suppose P2: x <= y1 ; :: thesis: Fodor_implication . (x,y1) <= Fodor_implication . (x,y2)

then x <= y2 by Z2, XXREAL_0:2;
then ( Fodor_implication . (x,y1) = 1 & Fodor_implication . (x,y2) = 1 ) by Fodor, P2;
hence Fodor_implication . (x,y1) <= Fodor_implication . (x,y2) ; :: thesis: verum

end;

suppose x > y1 ; :: thesis: Fodor_implication . (x,y1) <= Fodor_implication . (x,y2)

then P4: Fodor_implication . (x,y1) = max ((1 - x),y1) by Fodor;

per cases ( x <= y2 or x > y2 ) ;

suppose x <= y2 ; :: thesis: Fodor_implication . (x,y1) <= Fodor_implication . (x,y2)

then Fodor_implication . (x,y2) = 1 by Fodor;
hence Fodor_implication . (x,y1) <= Fodor_implication . (x,y2) by XXREAL_1:1; :: thesis: verum

end;

suppose x > y2 ; :: thesis: Fodor_implication . (x,y1) <= Fodor_implication . (x,y2)

then Fodor_implication . (x,y2) = max ((1 - x),y2) by Fodor;
hence Fodor_implication . (x,y1) <= Fodor_implication . (x,y2) by P4, Z2, XXREAL_0:26; :: thesis: verum

end;

end;

end;

end;

end;

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; :: thesis: verum