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)

proof

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;

hence t <= minnorm ; :: thesis: verum