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),f)))),(min ((1_minus g),g)))) . c by FUZZY_1:7

.= (max ((max ((min ((1_minus f),f)),(max ((min ((1_minus f),g)),(min ((1_minus g),f)))))),(min ((1_minus g),g)))) . c by FUZZY_1:7

.= (max ((max ((min ((1_minus f),g)),(min ((1_minus g),f)))),(max ((min ((1_minus f),f)),(min ((1_minus g),g)))))) . c by FUZZY_1:7

.= max (((f \+\ g) . c),((max ((min ((1_minus f),f)),(min ((1_minus g),g)))) . c)) by FUZZY_1:5 ;

hence (f \+\ g) . c <= ((max (f,g)) \ (min (f,g))) . c by XXREAL_0:25; :: thesis: verum

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),f)))),(min ((1_minus g),g)))) . c by FUZZY_1:7

.= (max ((max ((min ((1_minus f),f)),(max ((min ((1_minus f),g)),(min ((1_minus g),f)))))),(min ((1_minus g),g)))) . c by FUZZY_1:7

.= (max ((max ((min ((1_minus f),g)),(min ((1_minus g),f)))),(max ((min ((1_minus f),f)),(min ((1_minus g),g)))))) . c by FUZZY_1:7

.= max (((f \+\ g) . c),((max ((min ((1_minus f),f)),(min ((1_minus g),g)))) . c)) by FUZZY_1:5 ;

hence (f \+\ g) . c <= ((max (f,g)) \ (min (f,g))) . c by XXREAL_0:25; :: thesis: verum