let t be t-norm; :: thesis: drastic_norm <= t

set f1 = drastic_norm ;

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

set f1 = drastic_norm ;

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

proof

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

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

end;

suppose A2:
a = 1
; :: thesis: drastic_norm . (a,b) <= t . (a,b)

reconsider aa = 1, bb = b as Element of [.0,1.] by XXREAL_1:1;

t . (aa,bb) = t . (bb,aa) by BINOP_1:def 2

.= b by IdDef ;

hence drastic_norm . (a,b) <= t . (a,b) by DrasticDef, A2; :: thesis: verum

end;t . (aa,bb) = t . (bb,aa) by BINOP_1:def 2

.= b by IdDef ;

hence drastic_norm . (a,b) <= t . (a,b) by DrasticDef, A2; :: thesis: verum

suppose A2:
b = 1
; :: thesis: drastic_norm . (a,b) <= t . (a,b)

reconsider aa = a, bb = 1 as Element of [.0,1.] by XXREAL_1:1;

drastic_norm . (aa,bb) = aa by DrasticDef;

hence drastic_norm . (a,b) <= t . (a,b) by A2, IdDef; :: thesis: verum

end;drastic_norm . (aa,bb) = aa by DrasticDef;

hence drastic_norm . (a,b) <= t . (a,b) by A2, IdDef; :: thesis: verum

suppose A2:
( a <> 1 & b <> 1 )
; :: thesis: drastic_norm . (a,b) <= t . (a,b)

reconsider aa = a, bb = b as Element of [.0,1.] ;

drastic_norm . (aa,bb) = 0 by DrasticDef, A2;

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

end;drastic_norm . (aa,bb) = 0 by DrasticDef, A2;

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