let C be non empty set ; :: thesis: for f, h, g being Membership_Func of C st g c= holds
g \ h c=
let f, h, g 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 2 :: thesis: g \ h c=
let c be Element of C; :: according to FUZZY_1:def 2 :: 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:5;
hence (f \ h) . c <= (g \ h) . c by FUZZY_1:5; :: thesis: verum