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

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