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)

proof

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)

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

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;

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;

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;

end;

end;

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

proof

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)

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

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;

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;

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;

end;

end;

( 0 in [.0,1.] & 1 in [.0,1.] ) by XXREAL_1:1;
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