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

proof

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

per cases ;

suppose U1: x2 <= y ; :: thesis:

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

end;

suppose x2 > y ; :: thesis:

then U2: Rescher_implication . (x2,y) = 0 by Rescher;
thus Rescher_implication . (x1,y) >= Rescher_implication . (x2,y) by U2, Rescher; :: thesis:

end;

end;

end;

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

proof

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

per cases ;

suppose P2: x <= y1 ; :: thesis:

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

end;

suppose x > y1 ; :: thesis:

then Rescher_implication . (x,y1) = 0 by Rescher;
hence Rescher_implication . (x,y1) <= Rescher_implication . (x,y2) by Rescher; :: thesis:

end;

end;

end;

( 0 in [.0,1.] & 1 in [.0,1.] ) by XXREAL_1:1;
hence ( Rescher_implication is decreasing_on_1st & Rescher_implication is increasing_on_2nd & Rescher_implication is 00-dominant & Rescher_implication is 11-dominant & Rescher_implication is 10-weak ) by b0, ia, Rescher; :: thesis: