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

h c=

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

assume that

A1: for c being Element of C holds (f \ g) . c <= h . c and

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

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

A3: (min (g,(1_minus f))) . c <= h . c by A2;

(min (f,(1_minus g))) . c <= h . c by A1;

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

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

h c=

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

assume that

A1: for c being Element of C holds (f \ g) . c <= h . c and

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

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

A3: (min (g,(1_minus f))) . c <= h . c by A2;

(min (f,(1_minus g))) . c <= h . c by A1;

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

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