let C be non empty set ; :: thesis: for f, g being Membership_Func of C holds 1_minus (f \+\ g) c=
let f, g be Membership_Func of C; :: thesis: 1_minus (f \+\ g) c=
(max f,g) \ (min f,g) c= by Th25;
then 1_minus (f \+\ g) c= by FUZZY_1:39;
then 1_minus (f \+\ g) c= by FUZZY_1:12;
hence 1_minus (f \+\ g) c= ; :: thesis: verum