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 3 :: 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 Th8
.= max (min f,(1_minus g)),(min (max (min (1_minus f),g),f),(max g,(min (1_minus f),g))) by Th10
.= max (min f,(1_minus g)),(min (max (min (1_minus f),g),f),g) by Th9
.= min (max (min f,(1_minus g)),(max f,(min (1_minus f),g))),(max (min f,(1_minus g)),g) by Th10
.= min (max (max f,(min f,(1_minus g))),(min (1_minus f),g)),(max (min f,(1_minus g)),g) by Th8
.= min (max f,(min (1_minus f),g)),(max (min f,(1_minus g)),g) by Th9
.= min (min (max f,(1_minus f)),(max f,g)),(max g,(min f,(1_minus g))) by Th10
.= min (min (max f,(1_minus f)),(max f,g)),(min (max g,f),(max g,(1_minus g))) by Th10
.= min (min (min (max f,(1_minus f)),(max f,g)),(max g,f)),(max g,(1_minus g)) by Th8
.= min (min (max f,(1_minus f)),(min (max f,g),(max f,g))),(max g,(1_minus g)) by Th8
.= min (max f,g),(min (max f,(1_minus f)),(max g,(1_minus g))) by Th8 ;
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 Def4;
hence (max (f \+\ g),(min f,g)) . x <= (max f,g) . x by XXREAL_0:17; :: thesis: verum