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