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 ( g c= & max f,g c= ) by Th18, Th20;
hence max f,g = g by Lm1; :: thesis: verum