for a, b being Element of [.0,1.] holds maxnorm . (a,b) = 1 - (minnorm . ((1 - a),(1 - b)))

proof

let a, b be Element of [.0,1.]; :: thesis: maxnorm . (a,b) = 1 - (minnorm . ((1 - a),(1 - b)))
A1: ( 1 - a in [.0,1.] & 1 - b in [.0,1.] ) by OpIn01;
set e1 = - 1;
A2: - (max (((- 1) * (- a)),((- 1) * (- b)))) = - ((- 1) * (min ((- a),(- b)))) by MES57
.= min ((- a),(- b)) ;
A3: min ((1 + (- a)),(1 + (- b))) = 1 + (min ((- a),(- b))) by FUZZY_2:42
.= 1 - (max (a,b)) by A2 ;
maxnorm . (a,b) = 1 - (min ((1 - a),(1 - b))) by A3, MaxDef
.= 1 - (minnorm . ((1 - a),(1 - b))) by A1, MinDef ;
hence maxnorm . (a,b) = 1 - (minnorm . ((1 - a),(1 - b))) ; :: thesis: verum

end;

hence maxnorm = conorm minnorm by CoDef; :: thesis: verum