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:10;
hence max f,g c= by FUZZY_1:18; :: thesis: verum