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 3 :: 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:12
.= (max (min (max f,g),(1_minus f)),(min (max f,g),(1_minus g))) . c by FUZZY_1:10
.= (max (max (min (1_minus f),f),(min (1_minus f),g)),(min (1_minus g),(max f,g))) . c by FUZZY_1:10
.= (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:10
.= (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:8
.= (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:8
.= (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:8
.= max ((max (min (1_minus f),f),(min (1_minus g),g)) . c),((f \+\ g) . c) by FUZZY_1:6 ;
hence (f \+\ g) . c <= ((max f,g) \ (min f,g)) . c by XXREAL_0:25; :: thesis: verum