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 3 :: 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 Th12
.= min (max (1_minus f),(1_minus (1_minus g))),(1_minus (min (1_minus f),g)) by Th12
.= min (max (1_minus f),g),(max (1_minus (1_minus f)),(1_minus g)) by Th12
.= max (min (max (1_minus f),g),f),(min (max (1_minus f),g),(1_minus g)) by Th10
.= max (max (min f,(1_minus f)),(min f,g)),(min (max (1_minus f),g),(1_minus g)) by Th10
.= max (max (min f,(1_minus f)),(min f,g)),(max (min (1_minus g),(1_minus f)),(min (1_minus g),g)) by Th10
.= max (max (max (min f,g),(min f,(1_minus f))),(min (1_minus g),(1_minus f))),(min (1_minus g),g) by Th8
.= max (max (max (min (1_minus g),(1_minus f)),(min f,g)),(min f,(1_minus f))),(min (1_minus g),g) by Th8
.= max (max (min (1_minus g),(1_minus f)),(min f,g)),(max (min f,(1_minus f)),(min (1_minus g),g)) by Th8 ;
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 Def5;
hence (max (min f,g),(min (1_minus f),(1_minus g))) . x <= (1_minus (f \+\ g)) . x by XXREAL_0:25; :: thesis: verum