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:17;
hence (max (f,g)) \ g c= by Th4; :: thesis: verum