set f = Goedel_implication ;

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

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

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

hence ( Goedel_implication is decreasing_on_1st & Goedel_implication is increasing_on_2nd & Goedel_implication is 00-dominant & Goedel_implication is 11-dominant & Goedel_implication is 10-weak ) by a0, aa, Goedel; :: thesis: verum

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

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

proof

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

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

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

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

end;

suppose S1:
x2 <= y
; :: thesis: Goedel_implication . (x1,y) >= Goedel_implication . (x2,y)

then S2:
Goedel_implication . (x2,y) = 1
by Goedel;

x1 <= y by S1, Z0, XXREAL_0:2;

hence Goedel_implication . (x1,y) >= Goedel_implication . (x2,y) by S2, Goedel; :: thesis: verum

end;x1 <= y by S1, Z0, XXREAL_0:2;

hence Goedel_implication . (x1,y) >= Goedel_implication . (x2,y) by S2, Goedel; :: thesis: verum

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

then
( Goedel_implication . (x2,y) = y & Goedel_implication . (x1,y) = y )
by Goedel;

hence Goedel_implication . (x1,y) >= Goedel_implication . (x2,y) ; :: thesis: verum

end;hence Goedel_implication . (x1,y) >= Goedel_implication . (x2,y) ; :: thesis: verum

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

then
( Goedel_implication . (x2,y) = y & Goedel_implication . (x1,y) = 1 )
by Goedel;

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

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

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

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

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

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

end;

suppose Z1:
x <= y1
; :: thesis: Goedel_implication . (x,y1) <= Goedel_implication . (x,y2)

then Z3:
Goedel_implication . (x,y1) = 1
by Goedel;

x <= y2 by XXREAL_0:2, Z1, Z2;

hence Goedel_implication . (x,y1) <= Goedel_implication . (x,y2) by Z3, Goedel; :: thesis: verum

end;x <= y2 by XXREAL_0:2, Z1, Z2;

hence Goedel_implication . (x,y1) <= Goedel_implication . (x,y2) by Z3, Goedel; :: thesis: verum

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

then
( Goedel_implication . (x,y1) = y1 & Goedel_implication . (x,y2) = 1 )
by Goedel;

hence Goedel_implication . (x,y1) <= Goedel_implication . (x,y2) by XXREAL_1:1; :: thesis: verum

end;hence Goedel_implication . (x,y1) <= Goedel_implication . (x,y2) by XXREAL_1:1; :: thesis: verum

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

then
( Goedel_implication . (x,y1) = y1 & Goedel_implication . (x,y2) = y2 )
by Goedel;

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

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

hence ( Goedel_implication is decreasing_on_1st & Goedel_implication is increasing_on_2nd & Goedel_implication is 00-dominant & Goedel_implication is 11-dominant & Goedel_implication is 10-weak ) by a0, aa, Goedel; :: thesis: verum