defpred S₁[ set ] means ex x being object st
( x in X & $1 = Class (EqR,x) );
consider F being Subset-Family of X such that
A1: for A being Subset of X holds
( A in F iff S₁[A] ) from SUBSET_1:sch 3();
take F ; :: thesis: for A being Subset of X holds
( A in F iff ex x being object st
( x in X & A = Class (EqR,x) ) )
thus for A being Subset of X holds
( A in F iff ex x being object st
( x in X & A = Class (EqR,x) ) ) by A1; :: thesis: verum