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

h \ f c=

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

assume A1: for c being Element of C holds f . c <= g . c ; :: according to FUZZY_1:def 2 :: thesis: h \ f c=

let c be Element of C; :: according to FUZZY_1:def 2 :: thesis: (h \ g) . c <= (h \ f) . c

f . c <= g . c by A1;

then 1 - (f . c) >= 1 - (g . c) by XREAL_1:10;

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

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

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

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

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

h \ f c=

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

assume A1: for c being Element of C holds f . c <= g . c ; :: according to FUZZY_1:def 2 :: thesis: h \ f c=

let c be Element of C; :: according to FUZZY_1:def 2 :: thesis: (h \ g) . c <= (h \ f) . c

f . c <= g . c by A1;

then 1 - (f . c) >= 1 - (g . c) by XREAL_1:10;

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

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

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

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

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