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

proof

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

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

suppose U1: x2 < 1 ; :: thesis: Weber_implication . (x1,y) >= Weber_implication . (x2,y)

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

end;

suppose U6: x2 >= 1 ; :: thesis: Weber_implication . (x1,y) >= Weber_implication . (x2,y)

x2 <= 1 by XXREAL_1:1;
then u2: x2 = 1 by XXREAL_0:1, U6;

per cases ( ( x1 > y & x1 < 1 ) or ( x1 > y & x1 >= 1 ) or ( x1 <= y & x1 < 1 ) or ( x1 <= y & x1 >= 1 ) ) ;

suppose ( x1 > y & x1 < 1 ) ; :: thesis: Weber_implication . (x1,y) >= Weber_implication . (x2,y)

then Weber_implication . (x1,y) = 1 by Weber;
hence Weber_implication . (x1,y) >= Weber_implication . (x2,y) by XXREAL_1:1; :: thesis: verum

end;

suppose U5: ( x1 > y & x1 >= 1 ) ; :: thesis: Weber_implication . (x1,y) >= Weber_implication . (x2,y)

x1 <= 1 by XXREAL_1:1;
hence Weber_implication . (x1,y) >= Weber_implication . (x2,y) by u2, U5, XXREAL_0:1; :: thesis: verum

end;

suppose ( x1 <= y & x1 < 1 ) ; :: thesis: Weber_implication . (x1,y) >= Weber_implication . (x2,y)

then Weber_implication . (x1,y) = 1 by Weber;
hence Weber_implication . (x1,y) >= Weber_implication . (x2,y) by XXREAL_1:1; :: thesis: verum

end;

suppose IO: ( x1 <= y & x1 >= 1 ) ; :: thesis: Weber_implication . (x1,y) >= Weber_implication . (x2,y)

x1 <= 1 by XXREAL_1:1;
hence Weber_implication . (x1,y) >= Weber_implication . (x2,y) by u2, IO, XXREAL_0:1; :: thesis: verum

end;

end;

end;

end;

end;

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

proof

let x, y1, y2 be Element of [.0,1.]; :: thesis: ( y1 <= y2 implies Weber_implication . (x,y1) <= Weber_implication . (x,y2) )
P1: ( x >= 0 & x <= 1 ) by XXREAL_1:1;
assume Z2: y1 <= y2 ; :: thesis: Weber_implication . (x,y1) <= Weber_implication . (x,y2)

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

suppose x < 1 ; :: thesis: Weber_implication . (x,y1) <= Weber_implication . (x,y2)

then ( Weber_implication . (x,y1) = 1 & Weber_implication . (x,y2) = 1 ) by Weber;
hence Weber_implication . (x,y1) <= Weber_implication . (x,y2) ; :: thesis: verum

end;

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

then SS: x = 1 by XXREAL_0:1, P1;
then Weber_implication . (x,y1) = y1 by Weber;
hence Weber_implication . (x,y1) <= Weber_implication . (x,y2) by Z2, Weber, SS; :: thesis: verum

end;

end;

end;

( 0 in [.0,1.] & 1 in [.0,1.] ) by XXREAL_1:1;
hence ( Weber_implication is decreasing_on_1st & Weber_implication is increasing_on_2nd & Weber_implication is 00-dominant & Weber_implication is 11-dominant & Weber_implication is 10-weak ) by a0, b0, Weber; :: thesis: verum