let C be non empty set ; 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; ( 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
; FUZZY_1:def 2 h c=
let c be Element of C; FUZZY_1:def 2 (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; verum