let C be non empty set ; :: thesis: for f, g being Membership_Func of C st g c= holds
max (f,g) = g
let f, g be Membership_Func of C; :: thesis: ( g c= implies max (f,g) = g )
assume g c= ; :: thesis: max (f,g) = g
then A1: g c= by Th18;
max (f,g) c= by Th16;
hence max (f,g) = g by A1, Lm1; :: thesis: verum