let t be BinOp of [.0,1.]; conorm (conorm t) = t
set tt = conorm (conorm t);
for a, b being Element of [.0,1.] holds t . (a,b) = (conorm (conorm t)) . (a,b)
proof
let a,
b be
Element of
[.0,1.];
t . (a,b) = (conorm (conorm t)) . (a,b)
A1:
( 1
- a in [.0,1.] & 1
- b in [.0,1.] )
by OpIn01;
(conorm (conorm t)) . (
a,
b) =
1
- ((conorm t) . ((1 - a),(1 - b)))
by CoDef
.=
1
- (1 - (t . ((1 - (1 - a)),(1 - (1 - b)))))
by CoDef, A1
;
hence
t . (
a,
b)
= (conorm (conorm t)) . (
a,
b)
;
verum
end;
hence
conorm (conorm t) = t
by BINOP_1:2; verum