let F1, F2 be Subset-Family of X; :: thesis: ( ( for A being Subset of X holds
( A in F1 iff ex x being object st
( x in X & A = Class (EqR,x) ) ) ) & ( for A being Subset of X holds
( A in F2 iff ex x being object st
( x in X & A = Class (EqR,x) ) ) ) implies F1 = F2 )
assume that
A2: for A being Subset of X holds
( A in F1 iff ex x being object st
( x in X & A = Class (EqR,x) ) ) and
A3: for A being Subset of X holds
( A in F2 iff ex x being object st
( x in X & A = Class (EqR,x) ) ) ; :: thesis: F1 = F2

now :: thesis: for A being Subset of X holds
( A in F1 iff A in F2 )

let A be Subset of X; :: thesis: ( A in F1 iff A in F2 )
( A in F1 iff ex x being object st
( x in X & A = Class (EqR,x) ) ) by A2;
hence ( A in F1 iff A in F2 ) by A3; :: thesis: verum

end;

hence F1 = F2 by SETFAM_1:31; :: thesis: verum