let t be t-conorm; :: thesis: maxnorm <= t
set f1 = maxnorm ;
for a, b being Element of [.0,1.] holds maxnorm . (a,b) <= t . (a,b)

proof

let a, b be Element of [.0,1.]; :: thesis: maxnorm . (a,b) <= t . (a,b)
reconsider aa = a, bb = b as Element of [.0,1.] ;
A1: maxnorm . (a,b) = max (aa,bb) by MaxDef;
reconsider cc = 0 as Element of [.0,1.] by XXREAL_1:1;
aa >= 0 by XXREAL_1:1;
then t . (aa,bb) >= t . (cc,bb) by MonDef;
then t . (aa,bb) >= t . (bb,cc) by BINOP_1:def 2;
then A3: t . (aa,bb) >= bb by ZeroDef;
bb >= 0 by XXREAL_1:1;
then t . (aa,bb) >= t . (aa,cc) by MonDef;
then t . (aa,bb) >= aa by ZeroDef;
hence maxnorm . (a,b) <= t . (a,b) by A1, XXREAL_0:28, A3; :: thesis: verum

end;

hence maxnorm <= t ; :: thesis: verum