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 x be Element of C; :: according to FUZZY_1:def 2 :: thesis: (max ((f \+\ g),(min (f,g)))) . x <= (max (f,g)) . x
max ((f \+\ g),(min (f,g))) = max ((min (f,(1_minus g))),(max ((min ((1_minus f),g)),(min (f,g))))) by Th7
.= max ((min (f,(1_minus g))),(min ((max ((min ((1_minus f),g)),f)),(max (g,(min ((1_minus f),g))))))) by Th9
.= max ((min (f,(1_minus g))),(min ((max ((min ((1_minus f),g)),f)),g))) by Th8
.= min ((max ((min (f,(1_minus g))),(max (f,(min ((1_minus f),g)))))),(max ((min (f,(1_minus g))),g))) by Th9
.= min ((max ((max (f,(min (f,(1_minus g))))),(min ((1_minus f),g)))),(max ((min (f,(1_minus g))),g))) by Th7
.= min ((max (f,(min ((1_minus f),g)))),(max ((min (f,(1_minus g))),g))) by Th8
.= min ((min ((max (f,(1_minus f))),(max (f,g)))),(max (g,(min (f,(1_minus g)))))) by Th9
.= min ((min ((max (f,(1_minus f))),(max (f,g)))),(min ((max (g,f)),(max (g,(1_minus g)))))) by Th9
.= min ((min ((min ((max (f,(1_minus f))),(max (f,g)))),(max (g,f)))),(max (g,(1_minus g)))) by Th7
.= min ((min ((max (f,(1_minus f))),(min ((max (f,g)),(max (f,g)))))),(max (g,(1_minus g)))) by Th7
.= min ((max (f,g)),(min ((max (f,(1_minus f))),(max (g,(1_minus g)))))) by Th7 ;
then (max ((f \+\ g),(min (f,g)))) . x = min (((max (f,g)) . x),((min ((max (f,(1_minus f))),(max (g,(1_minus g))))) . x)) by Def3;
hence (max ((f \+\ g),(min (f,g)))) . x <= (max (f,g)) . x by XXREAL_0:17; :: thesis: verum