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

proof

let a, b be Element of [.0,1.]; :: thesis: drastic_conorm . (a,b) = 1 - (drastic_norm . ((1 - a),(1 - b)))
A3: ( 1 - a in [.0,1.] & 1 - b in [.0,1.] ) by OpIn01;
then we: ( 1 - a <= 1 & 1 - b <= 1 ) by XXREAL_1:1;
WE: ( 0 <= a & 0 <= b ) by XXREAL_1:1;

per cases ( ( a = 0 & b = 0 ) or ( a <> 0 & b <> 0 ) or ( b <> 0 & a = 0 ) or ( a <> 0 & b = 0 ) ) ;

suppose A0: ( a = 0 & b = 0 ) ; :: thesis: drastic_conorm . (a,b) = 1 - (drastic_norm . ((1 - a),(1 - b)))

then A1: min (a,b) = 0 ;
A2: max ((1 - a),(1 - b)) = 1 by A0;
drastic_conorm . (a,b) = max (a,b) by Drastic2CDef, A1
.= 1 - (min ((1 - a),(1 - b))) by A0
.= 1 - (drastic_norm . ((1 - a),(1 - b))) by Drastic2Def, A2, A3 ;
hence drastic_conorm . (a,b) = 1 - (drastic_norm . ((1 - a),(1 - b))) ; :: thesis: verum

end;

suppose BB: ( a <> 0 & b <> 0 ) ; :: thesis: drastic_conorm . (a,b) = 1 - (drastic_norm . ((1 - a),(1 - b)))

then B0: min (a,b) <> 0 by XXREAL_0:15;
( 1 - a <> 1 & 1 - b <> 1 ) by BB;
then B1: max ((1 - a),(1 - b)) <> 1 by XXREAL_0:16;
drastic_conorm . (a,b) = 1 - 0 by Drastic2CDef, B0
.= 1 - (drastic_norm . ((1 - a),(1 - b))) by Drastic2Def, B1, A3 ;
hence drastic_conorm . (a,b) = 1 - (drastic_norm . ((1 - a),(1 - b))) ; :: thesis: verum

end;

suppose BB: ( b <> 0 & a = 0 ) ; :: thesis: drastic_conorm . (a,b) = 1 - (drastic_norm . ((1 - a),(1 - b)))

then B0: min (a,b) = 0 by WE, XXREAL_0:def 9;
B1: min ((1 - a),(1 - b)) = 1 - b by we, XXREAL_0:def 9, BB;
B8: max ((1 - a),(1 - b)) = 1 by XXREAL_0:def 10, we, BB;
drastic_conorm . (a,b) = max (a,b) by Drastic2CDef, B0
.= 1 - (min ((1 - a),(1 - b))) by B1, BB, XXREAL_0:def 10, WE
.= 1 - (drastic_norm . ((1 - a),(1 - b))) by Drastic2Def, A3, B8 ;
hence drastic_conorm . (a,b) = 1 - (drastic_norm . ((1 - a),(1 - b))) ; :: thesis: verum

end;

suppose BB: ( a <> 0 & b = 0 ) ; :: thesis: drastic_conorm . (a,b) = 1 - (drastic_norm . ((1 - a),(1 - b)))

then B0: min (a,b) = 0 by WE, XXREAL_0:def 9;
B1: min ((1 - a),(1 - b)) = 1 - a by we, XXREAL_0:def 9, BB;
B8: max ((1 - a),(1 - b)) = 1 by XXREAL_0:def 10, we, BB;
drastic_conorm . (a,b) = max (a,b) by Drastic2CDef, B0
.= 1 - (min ((1 - a),(1 - b))) by B1, BB, XXREAL_0:def 10, WE
.= 1 - (drastic_norm . ((1 - a),(1 - b))) by Drastic2Def, A3, B8 ;
hence drastic_conorm . (a,b) = 1 - (drastic_norm . ((1 - a),(1 - b))) ; :: thesis: verum

end;

end;

end;

hence conorm drastic_norm = drastic_conorm by CoDef; :: thesis: verum