let C be non empty set ; :: thesis: for f, g being Membership_Func of C holds (max f,g) \ g c=
let f, g be Membership_Func of C; :: thesis: (max f,g) \ g c=
max f,g c= by FUZZY_1:18;
hence (max f,g) \ g c= by Th4; :: thesis: verum