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 Th20;

then 1_minus (f \+\ g) c= by FUZZY_1:36;

then 1_minus (f \+\ g) c= by FUZZY_1:11;

hence 1_minus (f \+\ g) c= ; :: thesis: verum

let f, g be Membership_Func of C; :: thesis: 1_minus (f \+\ g) c=

(max (f,g)) \ (min (f,g)) c= by Th20;

then 1_minus (f \+\ g) c= by FUZZY_1:36;

then 1_minus (f \+\ g) c= by FUZZY_1:11;

hence 1_minus (f \+\ g) c= ; :: thesis: verum