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=

max (f,(g \ f)) = min ((max (f,g)),(max (f,(1_minus f)))) by FUZZY_1:9;

hence max (f,g) c= by FUZZY_1:17; :: thesis: verum

let f, g be Membership_Func of C; :: thesis: max (f,g) c=

max (f,(g \ f)) = min ((max (f,g)),(max (f,(1_minus f)))) by FUZZY_1:9;

hence max (f,g) c= by FUZZY_1:17; :: thesis: verum