let C be non empty set ; :: thesis: for f, g being Membership_Func of C holds 1_minus (f \+\ g) c=
let f, g be Membership_Func of C; :: thesis: 1_minus (f \+\ g) c=
set f1 = 1_minus f;
set g1 = 1_minus g;
let x be Element of C; :: according to FUZZY_1:def 2 :: thesis: (max ((min (f,g)),(min ((1_minus f),(1_minus g))))) . x <= (1_minus (f \+\ g)) . x
1_minus (f \+\ g) = min ((1_minus (min (f,(1_minus g)))),(1_minus (min ((1_minus f),g)))) by Th10
.= min ((max ((1_minus f),(1_minus (1_minus g)))),(1_minus (min ((1_minus f),g)))) by Th10
.= min ((max ((1_minus f),g)),(max ((1_minus (1_minus f)),(1_minus g)))) by Th10
.= max ((min ((max ((1_minus f),g)),f)),(min ((max ((1_minus f),g)),(1_minus g)))) by Th9
.= max ((max ((min (f,(1_minus f))),(min (f,g)))),(min ((max ((1_minus f),g)),(1_minus g)))) by Th9
.= max ((max ((min (f,(1_minus f))),(min (f,g)))),(max ((min ((1_minus g),(1_minus f))),(min ((1_minus g),g))))) by Th9
.= max ((max ((max ((min (f,g)),(min (f,(1_minus f))))),(min ((1_minus g),(1_minus f))))),(min ((1_minus g),g))) by Th7
.= max ((max ((max ((min ((1_minus g),(1_minus f))),(min (f,g)))),(min (f,(1_minus f))))),(min ((1_minus g),g))) by Th7
.= max ((max ((min ((1_minus g),(1_minus f))),(min (f,g)))),(max ((min (f,(1_minus f))),(min ((1_minus g),g))))) by Th7 ;
then (1_minus (f \+\ g)) . x = max (((max ((min (f,g)),(min ((1_minus f),(1_minus g))))) . x),((max ((min (f,(1_minus f))),(min ((1_minus g),g)))) . x)) by Def4;
hence (max ((min (f,g)),(min ((1_minus f),(1_minus g))))) . x <= (1_minus (f \+\ g)) . x by XXREAL_0:25; :: thesis: verum