let C be non empty set ; :: thesis: for f, g being Membership_Func of C holds (max (f,g)) \ (min (f,g)) c=
let f, g be Membership_Func of C; :: thesis: (max (f,g)) \ (min (f,g)) c=
let c be Element of C; :: according to FUZZY_1:def 2 :: thesis: (f \+\ g) . c <= ((max (f,g)) \ (min (f,g))) . c
((max (f,g)) \ (min (f,g))) . c = (min ((max (f,g)),(max ((1_minus f),(1_minus g))))) . c by FUZZY_1:11
.= (max ((min ((max (f,g)),(1_minus f))),(min ((max (f,g)),(1_minus g))))) . c by FUZZY_1:9
.= (max ((max ((min ((1_minus f),f)),(min ((1_minus f),g)))),(min ((1_minus g),(max (f,g)))))) . c by FUZZY_1:9
.= (max ((max ((min ((1_minus f),f)),(min ((1_minus f),g)))),(max ((min ((1_minus g),f)),(min ((1_minus g),g)))))) . c by FUZZY_1:9
.= (max ((max ((max ((min ((1_minus f),f)),(min ((1_minus f),g)))),(min ((1_minus g),g)))),(min ((1_minus g),f)))) . c by FUZZY_1:7
.= (max ((max ((max ((min ((1_minus f),f)),(min ((1_minus g),g)))),(min ((1_minus f),g)))),(min ((1_minus g),f)))) . c by FUZZY_1:7
.= (max ((max ((min ((1_minus f),f)),(min ((1_minus g),g)))),(max ((min ((1_minus f),g)),(min ((1_minus g),f)))))) . c by FUZZY_1:7
.= max (((max ((min ((1_minus f),f)),(min ((1_minus g),g)))) . c),((f \+\ g) . c)) by FUZZY_1:5 ;
hence (f \+\ g) . c <= ((max (f,g)) \ (min (f,g))) . c by XXREAL_0:25; :: thesis: verum