let C be non empty set ; :: thesis: for f, h, g, h1 being Membership_Func of C st g c= & h1 c= holds

g \ h c=

let f, h, g, h1 be Membership_Func of C; :: thesis: ( g c= & h1 c= implies g \ h c= )

assume that

A1: for c being Element of C holds f . c <= g . c and

A2: for c being Element of C holds h . c <= h1 . 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 \ h1) . c <= (g \ h) . c

h . c <= h1 . c by A2;

then A3: 1 - (h . c) >= 1 - (h1 . c) by XREAL_1:10;

f . c <= g . c by A1;

then min ((f . c),(1 - (h1 . c))) <= min ((g . c),(1 - (h . c))) by A3, XXREAL_0:18;

then min ((f . c),((1_minus h1) . c)) <= min ((g . c),(1 - (h . c))) by FUZZY_1:def 5;

then min ((f . c),((1_minus h1) . c)) <= min ((g . c),((1_minus h) . c)) by FUZZY_1:def 5;

then (min (f,(1_minus h1))) . c <= min ((g . c),((1_minus h) . c)) by FUZZY_1:5;

hence (f \ h1) . c <= (g \ h) . c by FUZZY_1:5; :: thesis: verum

g \ h c=

let f, h, g, h1 be Membership_Func of C; :: thesis: ( g c= & h1 c= implies g \ h c= )

assume that

A1: for c being Element of C holds f . c <= g . c and

A2: for c being Element of C holds h . c <= h1 . 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 \ h1) . c <= (g \ h) . c

h . c <= h1 . c by A2;

then A3: 1 - (h . c) >= 1 - (h1 . c) by XREAL_1:10;

f . c <= g . c by A1;

then min ((f . c),(1 - (h1 . c))) <= min ((g . c),(1 - (h . c))) by A3, XXREAL_0:18;

then min ((f . c),((1_minus h1) . c)) <= min ((g . c),(1 - (h . c))) by FUZZY_1:def 5;

then min ((f . c),((1_minus h1) . c)) <= min ((g . c),((1_minus h) . c)) by FUZZY_1:def 5;

then (min (f,(1_minus h1))) . c <= min ((g . c),((1_minus h) . c)) by FUZZY_1:5;

hence (f \ h1) . c <= (g \ h) . c by FUZZY_1:5; :: thesis: verum