let F1, F2 be set ; :: thesis: ( ( for f being object holds
( f in F1 iff f is Membership_Func of X ) ) & ( for f being object holds
( f in F2 iff f is Membership_Func of X ) ) implies F1 = F2 )
assume that
E1: for x being object holds
( x in F1 iff x is Membership_Func of X ) and
E2: for x being object holds
( x in F2 iff x is Membership_Func of X ) ; :: thesis: F1 = F2
for x being object holds
( x in F1 iff x in F2 )

proof

let x be object ; :: thesis: ( x in F1 iff x in F2 )
( x in F1 iff x is Membership_Func of X ) by E1;
hence ( x in F1 iff x in F2 ) by E2; :: thesis: verum

end;

hence F1 = F2 by TARSKI:2; :: thesis: verum