let t be t-norm; 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.];
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;
verum
end;
hence
t <= minnorm
; verum