set f = Goguen_implication ;
a0: for x1, x2, y being Element of [.0,1.] st x1 <= x2 holds
Goguen_implication . (x1,y) >= Goguen_implication . (x2,y)

proof

let x1, x2, y be Element of [.0,1.]; :: thesis: ( x1 <= x2 implies Goguen_implication . (x1,y) >= Goguen_implication . (x2,y) )
assume Z0: x1 <= x2 ; :: thesis: Goguen_implication . (x1,y) >= Goguen_implication . (x2,y)

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

suppose U1: x2 <= y ; :: thesis: Goguen_implication . (x1,y) >= Goguen_implication . (x2,y)

then x1 <= y by Z0, XXREAL_0:2;
then ( Goguen_implication . (x1,y) = 1 & Goguen_implication . (x2,y) = 1 ) by Goguen, U1;
hence Goguen_implication . (x1,y) >= Goguen_implication . (x2,y) ; :: thesis: verum

end;

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

then U2: Goguen_implication . (x2,y) = y / x2 by Goguen;

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

suppose U5: x1 > y ; :: thesis: Goguen_implication . (x1,y) >= Goguen_implication . (x2,y)

then U3: Goguen_implication . (x1,y) = y / x1 by Goguen;
y >= 0 by XXREAL_1:1;
hence Goguen_implication . (x1,y) >= Goguen_implication . (x2,y) by U2, U3, Z0, XREAL_1:118, U5; :: thesis: verum

end;

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

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

end;

end;

end;

end;

end;

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

proof

let x, y1, y2 be Element of [.0,1.]; :: thesis: ( y1 <= y2 implies Goguen_implication . (x,y1) <= Goguen_implication . (x,y2) )
P1: x >= 0 by XXREAL_1:1;
assume Z2: y1 <= y2 ; :: thesis: Goguen_implication . (x,y1) <= Goguen_implication . (x,y2)

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

suppose P2: x <= y1 ; :: thesis: Goguen_implication . (x,y1) <= Goguen_implication . (x,y2)

then x <= y2 by Z2, XXREAL_0:2;
then ( Goguen_implication . (x,y1) = 1 & Goguen_implication . (x,y2) = 1 ) by Goguen, P2;
hence Goguen_implication . (x,y1) <= Goguen_implication . (x,y2) ; :: thesis: verum

end;

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

then P4: Goguen_implication . (x,y1) = y1 / x by Goguen;

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

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

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

end;

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

then Goguen_implication . (x,y2) = y2 / x by Goguen;
hence Goguen_implication . (x,y1) <= Goguen_implication . (x,y2) by P4, Z2, XREAL_1:72, P1; :: thesis: verum

end;

end;

end;

end;

end;

AA: ( 0 in [.0,1.] & 1 in [.0,1.] ) by XXREAL_1:1;
Goguen_implication . (1,0) = 0 / 1 by AA, Goguen
.= 0 ;
hence ( Goguen_implication is decreasing_on_1st & Goguen_implication is increasing_on_2nd & Goguen_implication is 00-dominant & Goguen_implication is 11-dominant & Goguen_implication is 10-weak ) by a0, aa, AA, Goguen; :: thesis: verum