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)
aa:
for x, y1, y2 being Element of [.0,1.] st y1 <= y2 holds
Goguen_implication . (x,y1) <= Goguen_implication . (x,y2)
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; verum