set f = Yager_implication ;

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

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

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

A2: Yager_implication . (1,1) = 1 to_power 1 by AA, Yager

.= 1 by POWER:26 ;

Yager_implication . (1,0) = 0 to_power 1 by AA, Yager

.= 0 by POWER:def 2 ;

hence ( Yager_implication is decreasing_on_1st & Yager_implication is increasing_on_2nd & Yager_implication is 00-dominant & Yager_implication is 11-dominant & Yager_implication is 10-weak ) by AA, A2, ai, b0, Yager; :: thesis: verum

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

Yager_implication . (x1,y) >= Yager_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 Yager_implication . (x1,y) >= Yager_implication . (x2,y) )

JI: ( 0 <= x1 & 0 <= x2 ) by XXREAL_1:1;

ZZ: ( 0 <= y & y <= 1 ) by XXREAL_1:1;

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

end;JI: ( 0 <= x1 & 0 <= x2 ) by XXREAL_1:1;

ZZ: ( 0 <= y & y <= 1 ) by XXREAL_1:1;

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

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

end;

suppose
( x2 = 0 & y = 0 )
; :: thesis: Yager_implication . (x1,y) >= Yager_implication . (x2,y)

end;

end;

suppose
( x2 <> 0 & x1 = 0 & y = 0 )
; :: thesis: Yager_implication . (x1,y) >= Yager_implication . (x2,y)

then
Yager_implication . (x1,y) = 1
by Yager;

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

end;hence Yager_implication . (x1,y) >= Yager_implication . (x2,y) by XXREAL_1:1; :: thesis: verum

suppose U6:
( x2 <> 0 & x1 <> 0 & y = 0 )
; :: thesis: Yager_implication . (x1,y) >= Yager_implication . (x2,y)

then u6:
( x1 > 0 & x2 > 0 )
by XXREAL_1:1;

u2: Yager_implication . (x1,y) = y to_power x1 by Yager, U6, JI

.= 0 by u6, U6, POWER:def 2 ;

Yager_implication . (x2,y) = y to_power x2 by Yager, U6, JI

.= 0 by JI, U6, POWER:def 2 ;

hence Yager_implication . (x1,y) >= Yager_implication . (x2,y) by u2; :: thesis: verum

end;u2: Yager_implication . (x1,y) = y to_power x1 by Yager, U6, JI

.= 0 by u6, U6, POWER:def 2 ;

Yager_implication . (x2,y) = y to_power x2 by Yager, U6, JI

.= 0 by JI, U6, POWER:def 2 ;

hence Yager_implication . (x1,y) >= Yager_implication . (x2,y) by u2; :: thesis: verum

suppose za:
y <> 0
; :: thesis: Yager_implication . (x1,y) >= Yager_implication . (x2,y)

then u2:
Yager_implication . (x1,y) = y to_power x1
by ZZ, Yager;

U2: Yager_implication . (x2,y) = y to_power x2 by Yager, za, ZZ;

end;U2: Yager_implication . (x2,y) = y to_power x2 by Yager, za, ZZ;

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

end;

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

( 0 < y & y < 1 & x1 < x2 )
by zz, za, ZZ, Z0, XXREAL_0:1;

hence Yager_implication . (x1,y) >= Yager_implication . (x2,y) by U2, u2, POWER:40; :: thesis: verum

end;hence Yager_implication . (x1,y) >= Yager_implication . (x2,y) by U2, u2, POWER:40; :: thesis: verum

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

1 >= 1 to_power x2
by POWER:26;

hence Yager_implication . (x1,y) >= Yager_implication . (x2,y) by U2, u2, zz, POWER:26; :: thesis: verum

end;hence Yager_implication . (x1,y) >= Yager_implication . (x2,y) by U2, u2, zz, POWER:26; :: thesis: verum

Yager_implication . (x,y1) <= Yager_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 Yager_implication . (x,y1) <= Yager_implication . (x,y2) )

assume Z2: y1 <= y2 ; :: thesis: Yager_implication . (x,y1) <= Yager_implication . (x,y2)

end;assume Z2: y1 <= y2 ; :: thesis: Yager_implication . (x,y1) <= Yager_implication . (x,y2)

per cases
( ( x = 0 & y2 = 0 ) or x <> 0 or y2 <> 0 )
;

end;

suppose P2:
( x = 0 & y2 = 0 )
; :: thesis: Yager_implication . (x,y1) <= Yager_implication . (x,y2)

0 <= y1
by XXREAL_1:1;

hence Yager_implication . (x,y1) <= Yager_implication . (x,y2) by P2, Z2; :: thesis: verum

end;hence Yager_implication . (x,y1) <= Yager_implication . (x,y2) by P2, Z2; :: thesis: verum

suppose P8:
x <> 0
; :: thesis: Yager_implication . (x,y1) <= Yager_implication . (x,y2)

su:
( x >= 0 & y2 >= 0 )
by XXREAL_1:1;

then P4: Yager_implication . (x,y2) = y2 to_power x by Yager, P8;

end;then P4: Yager_implication . (x,y2) = y2 to_power x by Yager, P8;

per cases
( ( y1 = 0 & x = 0 ) or ( y1 = 0 & x <> 0 ) or y1 <> 0 )
;

end;

suppose
( y1 = 0 & x = 0 )
; :: thesis: Yager_implication . (x,y1) <= Yager_implication . (x,y2)

end;

end;

suppose
( y1 = 0 & x <> 0 )
; :: thesis: Yager_implication . (x,y1) <= Yager_implication . (x,y2)

then p4:
Yager_implication . (x,y1) = y1 to_power x
by Yager, su;

y1 >= 0 by XXREAL_1:1;

hence Yager_implication . (x,y1) <= Yager_implication . (x,y2) by p4, P4, HOLDER_1:3, Z2, su; :: thesis: verum

end;y1 >= 0 by XXREAL_1:1;

hence Yager_implication . (x,y1) <= Yager_implication . (x,y2) by p4, P4, HOLDER_1:3, Z2, su; :: thesis: verum

suppose sy:
y1 <> 0
; :: thesis: Yager_implication . (x,y1) <= Yager_implication . (x,y2)

y1 >= 0
by XXREAL_1:1;

then p4: Yager_implication . (x,y1) = y1 to_power x by Yager, sy;

y1 >= 0 by XXREAL_1:1;

hence Yager_implication . (x,y1) <= Yager_implication . (x,y2) by p4, P4, HOLDER_1:3, Z2, su; :: thesis: verum

end;then p4: Yager_implication . (x,y1) = y1 to_power x by Yager, sy;

y1 >= 0 by XXREAL_1:1;

hence Yager_implication . (x,y1) <= Yager_implication . (x,y2) by p4, P4, HOLDER_1:3, Z2, su; :: thesis: verum

suppose P8:
y2 <> 0
; :: thesis: Yager_implication . (x,y1) <= Yager_implication . (x,y2)

su:
( x >= 0 & y2 >= 0 )
by XXREAL_1:1;

then P4: Yager_implication . (x,y2) = y2 to_power x by Yager, P8;

end;then P4: Yager_implication . (x,y2) = y2 to_power x by Yager, P8;

per cases
( ( y1 = 0 & x = 0 ) or ( y1 = 0 & x <> 0 ) or y1 <> 0 )
;

end;

suppose pg:
( y1 = 0 & x = 0 )
; :: thesis: Yager_implication . (x,y1) <= Yager_implication . (x,y2)

then
Yager_implication . (x,y1) = 1
by Yager;

hence Yager_implication . (x,y1) <= Yager_implication . (x,y2) by P4, POWER:24, pg; :: thesis: verum

end;hence Yager_implication . (x,y1) <= Yager_implication . (x,y2) by P4, POWER:24, pg; :: thesis: verum

suppose
( y1 = 0 & x <> 0 )
; :: thesis: Yager_implication . (x,y1) <= Yager_implication . (x,y2)

then p4:
Yager_implication . (x,y1) = y1 to_power x
by Yager, su;

y1 >= 0 by XXREAL_1:1;

hence Yager_implication . (x,y1) <= Yager_implication . (x,y2) by p4, P4, HOLDER_1:3, Z2, su; :: thesis: verum

end;y1 >= 0 by XXREAL_1:1;

hence Yager_implication . (x,y1) <= Yager_implication . (x,y2) by p4, P4, HOLDER_1:3, Z2, su; :: thesis: verum

suppose sy:
y1 <> 0
; :: thesis: Yager_implication . (x,y1) <= Yager_implication . (x,y2)

y1 >= 0
by XXREAL_1:1;

then p4: Yager_implication . (x,y1) = y1 to_power x by Yager, sy;

y1 >= 0 by XXREAL_1:1;

hence Yager_implication . (x,y1) <= Yager_implication . (x,y2) by p4, P4, HOLDER_1:3, Z2, su; :: thesis: verum

end;then p4: Yager_implication . (x,y1) = y1 to_power x by Yager, sy;

y1 >= 0 by XXREAL_1:1;

hence Yager_implication . (x,y1) <= Yager_implication . (x,y2) by p4, P4, HOLDER_1:3, Z2, su; :: thesis: verum

A2: Yager_implication . (1,1) = 1 to_power 1 by AA, Yager

.= 1 by POWER:26 ;

Yager_implication . (1,0) = 0 to_power 1 by AA, Yager

.= 0 by POWER:def 2 ;

hence ( Yager_implication is decreasing_on_1st & Yager_implication is increasing_on_2nd & Yager_implication is 00-dominant & Yager_implication is 11-dominant & Yager_implication is 10-weak ) by AA, A2, ai, b0, Yager; :: thesis: verum