for C being non empty set
for f, g being Membership_Func of C holds
( f = g iff ( g c= & f c= ) ) by Lm1;