let C be non empty set ; :: thesis: for f, g, h being Membership_Func of C st g c= holds
g \ h c=
let f, g, h be Membership_Func of C; :: thesis: ( g c= implies g \ h c= )
assume A1: for c being Element of C holds f . c <= g . c ; :: according to FUZZY_1:def 3 :: thesis: g \ h c=
let c be Element of C; :: according to FUZZY_1:def 3 :: thesis: (f \ h) . c <= (g \ h) . c
f . c <= g . c by A1;
then min (f . c),((1_minus h) . c) <= min (g . c),((1_minus h) . c) by XXREAL_0:18;
then (f \ h) . c <= min (g . c),((1_minus h) . c) by FUZZY_1:6;
hence (f \ h) . c <= (g \ h) . c by FUZZY_1:6; :: thesis: verum