defpred S₁[ set ] means ex x being set 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 set st
( x in X & A = Class EqR,x ) )
thus for A being Subset of X holds
( A in F iff ex x being set st
( x in X & A = Class EqR,x ) ) by A1; :: thesis: verum