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)

set f1 = maxnorm ;

for a, b being Element of [.0,1.] holds maxnorm . (a,b) <= t . (a,b)

proof

hence
maxnorm <= t
; :: thesis: verum
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;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