set dn = conorm nilmin_norm;
set dc = nilmax_conorm ;
for a, b being Element of [.0,1.] holds nilmax_conorm . (a,b) = 1 - (nilmin_norm . ((1 - a),(1 - b)))

proof

let a, b be Element of [.0,1.]; :: thesis: nilmax_conorm . (a,b) = 1 - (nilmin_norm . ((1 - a),(1 - b)))
A3: ( 1 - a in [.0,1.] & 1 - b in [.0,1.] ) by OpIn01;

per cases ( a + b < 1 or a + b >= 1 ) ;

suppose W0: a + b < 1 ; :: thesis: nilmax_conorm . (a,b) = 1 - (nilmin_norm . ((1 - a),(1 - b)))

then 2 - (a + b) > 2 - 1 by XREAL_1:10;
then W1: (1 - a) + (1 - b) > 1 ;
nilmax_conorm . (a,b) = max (a,b) by NilmaxDef, W0
.= 1 - (min ((1 - a),(1 - b))) by MaxMin
.= 1 - (nilmin_norm . ((1 - a),(1 - b))) by NilminDef, A3, W1 ;
hence nilmax_conorm . (a,b) = 1 - (nilmin_norm . ((1 - a),(1 - b))) ; :: thesis: verum

end;

suppose W0: a + b >= 1 ; :: thesis: nilmax_conorm . (a,b) = 1 - (nilmin_norm . ((1 - a),(1 - b)))

then 2 - (a + b) <= 2 - 1 by XREAL_1:10;
then W1: (1 - a) + (1 - b) <= 1 ;
nilmax_conorm . (a,b) = 1 - 0 by NilmaxDef, W0
.= 1 - (nilmin_norm . ((1 - a),(1 - b))) by NilminDef, A3, W1 ;
hence nilmax_conorm . (a,b) = 1 - (nilmin_norm . ((1 - a),(1 - b))) ; :: thesis: verum

end;

end;

end;

hence conorm nilmin_norm = nilmax_conorm by CoDef; :: thesis: verum