let C be non empty set ; for f, g, h being Membership_Func of C st h c= & h c= holds
h c=
let f, g, h 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 3 h c=
let c be Element of C; FUZZY_1:def 3 (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:6; verum