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

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