let t be t-conorm; :: thesis: t <= drastic_conorm
set f1 = drastic_conorm ;
for a, b being Element of [.0,1.] holds drastic_conorm . (a,b) >= t . (a,b)

proof

let a, b be Element of [.0,1.]; :: thesis: drastic_conorm . (a,b) >= t . (a,b)

per cases ( a = 0 or b = 0 or min (a,b) <> 0 ) by XXREAL_0:15;

suppose A2: a = 0 ; :: thesis: drastic_conorm . (a,b) >= t . (a,b)

then reconsider aa = 0 , bb = b as Element of [.0,1.] ;
aa <= bb by XXREAL_1:1;
then min (aa,bb) = 0 by XXREAL_0:def 9;
then A3: drastic_conorm . (aa,bb) = max (aa,bb) by Drastic2CDef;
t . (aa,bb) = t . (bb,aa) by BINOP_1:def 2
.= b by ZeroDef ;
hence drastic_conorm . (a,b) >= t . (a,b) by A2, A3, XXREAL_0:25; :: thesis: verum

end;

suppose A2: b = 0 ; :: thesis: drastic_conorm . (a,b) >= t . (a,b)

then reconsider aa = a, bb = 0 as Element of [.0,1.] ;
aa >= bb by XXREAL_1:1;
then min (aa,bb) = 0 by XXREAL_0:def 9;
then A3: drastic_conorm . (aa,bb) = max (aa,bb) by Drastic2CDef;
t . (aa,bb) = a by ZeroDef;
hence drastic_conorm . (a,b) >= t . (a,b) by A2, A3, XXREAL_0:25; :: thesis: verum

end;

suppose aa: min (a,b) <> 0 ; :: thesis: drastic_conorm . (a,b) >= t . (a,b)

reconsider aa = a, bb = b as Element of [.0,1.] ;
drastic_conorm . (aa,bb) = 1 by Drastic2CDef, aa;
hence drastic_conorm . (a,b) >= t . (a,b) by XXREAL_1:1; :: thesis: verum

end;

end;

end;

hence t <= drastic_conorm ; :: thesis: verum