let C be non empty set ; :: thesis: for f, g, h, h1 being Membership_Func of C st g c= & h1 c= holds
g \ h c=
let f, g, h, 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 3 :: thesis: g \ h c=
let c be Element of C; :: according to FUZZY_1:def 3 :: thesis: (f \ h1) . c <= (g \ h) . c
h . c <= h1 . c by A2;
then A3: 1 - (h . c) >= 1 - (h1 . c) by XREAL_1:12;
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 6;
then min (f . c),((1_minus h1) . c) <= min (g . c),((1_minus h) . c) by FUZZY_1:def 6;
then (min f,(1_minus h1)) . c <= min (g . c),((1_minus h) . c) by FUZZY_1:6;
hence (f \ h1) . c <= (g \ h) . c by FUZZY_1:6; :: thesis: verum