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