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)

set f1 = drastic_conorm ;

for a, b being Element of [.0,1.] holds drastic_conorm . (a,b) >= t . (a,b)

proof

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

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

end;

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;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

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;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

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;drastic_conorm . (aa,bb) = 1 by Drastic2CDef, aa;

hence drastic_conorm . (a,b) >= t . (a,b) by XXREAL_1:1; :: thesis: verum