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

( 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 )

hence
F1 = F2
by SETFAM_1:31; :: thesis: verum( 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;( 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