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 )

( 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

hence
F1 = F2
by TARSKI:2; :: thesis: verum
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;( x in F1 iff x is Membership_Func of X ) by E1;

hence ( x in F1 iff x in F2 ) by E2; :: thesis: verum