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)

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

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

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

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

proof

aa:
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 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;( 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

Reichenbach_implication . (x,y1) <= Reichenbach_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 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;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

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