let t be t-conorm; :: thesis:
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 ; :: 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 ; :: 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 ;
hence drastic_conorm . (a,b) >= t . (a,b) by XXREAL_1:1; :: thesis: verum
end;
end;
end;
hence t <= drastic_conorm ; :: thesis: verum