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 3 :: 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:8
.= max (min f,(1_minus g)),(min (max (min (1_minus f),g),f),(max (min (1_minus f),g),g)) by FUZZY_1:10
.= max (min f,(1_minus g)),(min (max (min (1_minus f),g),f),g) by FUZZY_1:9
.= min (max (min f,(1_minus g)),(max (min (1_minus f),g),f)),(max (min f,(1_minus g)),g) by FUZZY_1:10 ;
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:6;
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:10
.= min ((max f,g) . c),((max g,(1_minus g)) . c) by FUZZY_1:6 ;
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