let t be t-norm; :: thesis: t <= minnorm

set f1 = minnorm ;

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

set f1 = minnorm ;

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

proof

hence
t <= minnorm
; :: thesis: verum
let a, b be Element of [.0,1.]; :: thesis: t . (a,b) <= minnorm . (a,b)

reconsider aa = a, bb = b as Element of [.0,1.] ;

A1: minnorm . (a,b) = min (aa,bb) by MinDef;

reconsider cc = 1 as Element of [.0,1.] by XXREAL_1:1;

aa <= 1 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 IdDef;

bb <= 1 by XXREAL_1:1;

then t . (aa,bb) <= t . (aa,cc) by MonDef;

then t . (aa,bb) <= aa by IdDef;

hence t . (a,b) <= minnorm . (a,b) by A1, XXREAL_0:20, A3; :: thesis: verum

end;reconsider aa = a, bb = b as Element of [.0,1.] ;

A1: minnorm . (a,b) = min (aa,bb) by MinDef;

reconsider cc = 1 as Element of [.0,1.] by XXREAL_1:1;

aa <= 1 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 IdDef;

bb <= 1 by XXREAL_1:1;

then t . (aa,bb) <= t . (aa,cc) by MonDef;

then t . (aa,bb) <= aa by IdDef;

hence t . (a,b) <= minnorm . (a,b) by A1, XXREAL_0:20, A3; :: thesis: verum