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)

proof

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

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

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;

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;

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;

end;

end;

hence drastic_norm <= t ; :: thesis: verum