set f = Lukasiewicz_implication ;

A1: ( 0 in [.0,1.] & 1 in [.0,1.] ) by XXREAL_1:1;

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

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

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

min (1,((1 - 0) + 0)) = 1 ;

hence ( Lukasiewicz_implication is decreasing_on_1st & Lukasiewicz_implication is increasing_on_2nd & Lukasiewicz_implication is 00-dominant & Lukasiewicz_implication is 11-dominant & Lukasiewicz_implication is 10-weak ) by b1, b3, A1, Luk, bb; :: thesis: verum

A1: ( 0 in [.0,1.] & 1 in [.0,1.] ) by XXREAL_1:1;

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

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

proof

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

assume U1: x1 <= x2 ; :: thesis: Lukasiewicz_implication . (x1,y) >= Lukasiewicz_implication . (x2,y)

U2: Lukasiewicz_implication . (x1,y) = min (1,((1 - x1) + y)) by Luk;

U3: Lukasiewicz_implication . (x2,y) = min (1,((1 - x2) + y)) by Luk;

1 - x1 >= 1 - x2 by U1, XREAL_1:13;

then (1 - x1) + y >= (1 - x2) + y by XREAL_1:7;

hence Lukasiewicz_implication . (x1,y) >= Lukasiewicz_implication . (x2,y) by U2, U3, XXREAL_0:18; :: thesis: verum

end;assume U1: x1 <= x2 ; :: thesis: Lukasiewicz_implication . (x1,y) >= Lukasiewicz_implication . (x2,y)

U2: Lukasiewicz_implication . (x1,y) = min (1,((1 - x1) + y)) by Luk;

U3: Lukasiewicz_implication . (x2,y) = min (1,((1 - x2) + y)) by Luk;

1 - x1 >= 1 - x2 by U1, XREAL_1:13;

then (1 - x1) + y >= (1 - x2) + y by XREAL_1:7;

hence Lukasiewicz_implication . (x1,y) >= Lukasiewicz_implication . (x2,y) by U2, U3, XXREAL_0:18; :: thesis: verum

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

proof

bb:
min (1,((1 - 1) + 0)) = 0
by XXREAL_0:def 9;
let x, y1, y2 be Element of [.0,1.]; :: thesis: ( y1 <= y2 implies Lukasiewicz_implication . (x,y1) <= Lukasiewicz_implication . (x,y2) )

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

then (1 - x) + y1 <= (1 - x) + y2 by XREAL_1:7;

then U1: min (1,((1 - x) + y2)) >= min (1,((1 - x) + y1)) by XXREAL_0:18;

Lukasiewicz_implication . (x,y1) = min (1,((1 - x) + y1)) by Luk;

hence Lukasiewicz_implication . (x,y1) <= Lukasiewicz_implication . (x,y2) by U1, Luk; :: thesis: verum

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

then (1 - x) + y1 <= (1 - x) + y2 by XREAL_1:7;

then U1: min (1,((1 - x) + y2)) >= min (1,((1 - x) + y1)) by XXREAL_0:18;

Lukasiewicz_implication . (x,y1) = min (1,((1 - x) + y1)) by Luk;

hence Lukasiewicz_implication . (x,y1) <= Lukasiewicz_implication . (x,y2) by U1, Luk; :: thesis: verum

min (1,((1 - 0) + 0)) = 1 ;

hence ( Lukasiewicz_implication is decreasing_on_1st & Lukasiewicz_implication is increasing_on_2nd & Lukasiewicz_implication is 00-dominant & Lukasiewicz_implication is 11-dominant & Lukasiewicz_implication is 10-weak ) by b1, b3, A1, Luk, bb; :: thesis: verum