defpred S_{1}[ 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_{1}[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

( 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

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