let t1, t2 be t-norm; ( t1 <= t2 implies conorm t2 <= conorm t1 )
set c1 = conorm t1;
set c2 = conorm t2;
assume A1:
t1 <= t2
; conorm t2 <= conorm t1
for a, b being Element of [.0,1.] holds (conorm t2) . (a,b) <= (conorm t1) . (a,b)
proof
let a,
b be
Element of
[.0,1.];
(conorm t2) . (a,b) <= (conorm t1) . (a,b)
( 1
- a in [.0,1.] & 1
- b in [.0,1.] )
by OpIn01;
then
1
- (t2 . ((1 - a),(1 - b))) <= 1
- (t1 . ((1 - a),(1 - b)))
by A1, XREAL_1:10;
then
1
- (t2 . ((1 - a),(1 - b))) <= (conorm t1) . (
a,
b)
by CoDef;
hence
(conorm t2) . (
a,
b)
<= (conorm t1) . (
a,
b)
by CoDef;
verum
end;
hence
conorm t2 <= conorm t1
; verum