let t1, t2 be t-norm; :: thesis: ( t1 <= t2 implies conorm t2 <= conorm t1 )
set c1 = conorm t1;
set c2 = conorm t2;
assume A1: t1 <= t2 ; :: thesis: 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.]; :: thesis: (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; :: thesis: verum

end;

hence conorm t2 <= conorm t1 ; :: thesis: verum