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)

Fodor_implication . (x,y1) <= Fodor_implication . (x,y2)

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

a0: for x1, x2, y being Element of [.0,1.] st x1 <= x2 holds

Fodor_implication . (x1,y) >= Fodor_implication . (x2,y)

proof

b0:
for x, y1, y2 being Element of [.0,1.] st y1 <= y2 holds
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)

end;assume Z0: x1 <= x2 ; :: thesis: Fodor_implication . (x1,y) >= Fodor_implication . (x2,y)

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

end;

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;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

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

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

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

end;

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;- 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

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;hence Fodor_implication . (x1,y) >= Fodor_implication . (x2,y) by XXREAL_1:1; :: thesis: verum

Fodor_implication . (x,y1) <= Fodor_implication . (x,y2)

proof

AA:
( 0 in [.0,1.] & 1 in [.0,1.] )
by XXREAL_1:1;
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)

end;assume Z2: y1 <= y2 ; :: thesis: Fodor_implication . (x,y1) <= Fodor_implication . (x,y2)

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

end;

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;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

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

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

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

end;

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;hence Fodor_implication . (x,y1) <= Fodor_implication . (x,y2) by XXREAL_1:1; :: thesis: verum

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;hence Fodor_implication . (x,y1) <= Fodor_implication . (x,y2) by P4, Z2, XXREAL_0:26; :: thesis: verum

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