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