set f = Reichenbach_implication ;
a0: for x1, x2, y being Element of [.0,1.] st x1 <= x2 holds
Reichenbach_implication . (x1,y) >= Reichenbach_implication . (x2,y)

proof

let x1, x2, y be Element of [.0,1.]; :: thesis: ( x1 <= x2 implies Reichenbach_implication . (x1,y) >= Reichenbach_implication . (x2,y) )
( 0 <= y & y <= 1 ) by XXREAL_1:1;
then - 1 <= - y by XREAL_1:24;
then zs: 1 + (- 1) <= 1 + (- y) by XREAL_1:7;
assume x1 <= x2 ; :: thesis: Reichenbach_implication . (x1,y) >= Reichenbach_implication . (x2,y)
then - x2 <= - x1 by XREAL_1:24;
then (- x2) * (1 - y) <= (- x1) * (1 - y) by zs, XREAL_1:64;
then 1 + ((- x2) * (1 - y)) <= 1 + ((- x1) * (1 - y)) by XREAL_1:7;
then (1 - x2) + (x2 * y) <= (1 - x1) + (x1 * y) ;
then Reichenbach_implication . (x2,y) <= (1 - x1) + (x1 * y) by Reichen;
hence Reichenbach_implication . (x1,y) >= Reichenbach_implication . (x2,y) by Reichen; :: thesis: verum

end;

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

proof

let x, y1, y2 be Element of [.0,1.]; :: thesis: ( y1 <= y2 implies Reichenbach_implication . (x,y1) <= Reichenbach_implication . (x,y2) )
P1: x >= 0 by XXREAL_1:1;
assume y1 <= y2 ; :: thesis: Reichenbach_implication . (x,y1) <= Reichenbach_implication . (x,y2)
then x * y1 <= x * y2 by XREAL_1:64, P1;
then (1 - x) + (x * y1) <= (1 - x) + (x * y2) by XREAL_1:7;
then Reichenbach_implication . (x,y1) <= (1 - x) + (x * y2) by Reichen;
hence Reichenbach_implication . (x,y1) <= Reichenbach_implication . (x,y2) by Reichen; :: thesis: verum

end;

AA: ( 0 in [.0,1.] & 1 in [.0,1.] ) by XXREAL_1:1;
then A1: Reichenbach_implication . (0,0) = (1 - 0) + (0 * 0) by Reichen
.= 1 ;
A2: Reichenbach_implication . (1,1) = (1 - 1) + (1 * 1) by AA, Reichen
.= 1 ;
Reichenbach_implication . (1,0) = (1 - 1) + (1 * 0) by AA, Reichen;
hence ( Reichenbach_implication is decreasing_on_1st & Reichenbach_implication is increasing_on_2nd & Reichenbach_implication is 00-dominant & Reichenbach_implication is 11-dominant & Reichenbach_implication is 10-weak ) by A1, A2, a0, aa; :: thesis: verum