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)

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

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

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

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

proof

b0:
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 Weber_implication . (x1,y) >= Weber_implication . (x2,y) )

assume Z0: x1 <= x2 ; :: thesis: Weber_implication . (x1,y) >= Weber_implication . (x2,y)

end;assume Z0: x1 <= x2 ; :: thesis: Weber_implication . (x1,y) >= Weber_implication . (x2,y)

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

end;

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;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

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;

end;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 ) )
;

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;hence Weber_implication . (x1,y) >= Weber_implication . (x2,y) by XXREAL_1:1; :: thesis: verum

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;hence Weber_implication . (x1,y) >= Weber_implication . (x2,y) by u2, U5, XXREAL_0:1; :: thesis: verum

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;hence Weber_implication . (x1,y) >= Weber_implication . (x2,y) by XXREAL_1:1; :: thesis: verum

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;hence Weber_implication . (x1,y) >= Weber_implication . (x2,y) by u2, IO, XXREAL_0:1; :: thesis: verum

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

proof

( 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 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)

end;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 )
;

end;

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;hence Weber_implication . (x,y1) <= Weber_implication . (x,y2) ; :: thesis: verum

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;then Weber_implication . (x,y1) = y1 by Weber;

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

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