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

proof

let x1, x2, y be Element of [.0,1.]; :: thesis: ( x1 <= x2 implies Kleene-Dienes_implication . (x1,y) >= Kleene-Dienes_implication . (x2,y) )
assume x1 <= x2 ; :: thesis: Kleene-Dienes_implication . (x1,y) >= Kleene-Dienes_implication . (x2,y)
then - x2 <= - x1 by XREAL_1:24;
then 1 + (- x2) <= 1 + (- x1) by XREAL_1:7;
then max ((1 - x2),y) <= max ((1 - x1),y) by XXREAL_0:26;
then Kleene-Dienes_implication . (x2,y) <= max ((1 - x1),y) by Kleene;
hence Kleene-Dienes_implication . (x1,y) >= Kleene-Dienes_implication . (x2,y) by Kleene; :: thesis: verum

end;

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

proof

let x, y1, y2 be Element of [.0,1.]; :: thesis: ( y1 <= y2 implies Kleene-Dienes_implication . (x,y1) <= Kleene-Dienes_implication . (x,y2) )
assume y1 <= y2 ; :: thesis: Kleene-Dienes_implication . (x,y1) <= Kleene-Dienes_implication . (x,y2)
then max ((1 - x),y1) <= max ((1 - x),y2) by XXREAL_0:26;
then max ((1 - x),y1) <= Kleene-Dienes_implication . (x,y2) by Kleene;
hence Kleene-Dienes_implication . (x,y1) <= Kleene-Dienes_implication . (x,y2) by Kleene; :: thesis: verum

end;

AA: ( 0 in [.0,1.] & 1 in [.0,1.] ) by XXREAL_1:1;
then A1: Kleene-Dienes_implication . (0,0) = max ((1 - 0),0) by Kleene
.= 1 by XXREAL_0:def 10 ;
A2: Kleene-Dienes_implication . (1,1) = max ((1 - 1),1) by AA, Kleene
.= 1 by XXREAL_0:def 10 ;
Kleene-Dienes_implication . (1,0) = max ((1 - 1),0) by AA, Kleene
.= 0 ;
hence ( Kleene-Dienes_implication is decreasing_on_1st & Kleene-Dienes_implication is increasing_on_2nd & Kleene-Dienes_implication is 00-dominant & Kleene-Dienes_implication is 11-dominant & Kleene-Dienes_implication is 10-weak ) by A1, A2, a0, aa; :: thesis: verum