defpred S₁[ Subset of ] means ex B being Subset of st
( B in G & $1 = f " B );
ex R being Subset-Family of st
for A being Subset of holds
( A in R iff S₁[A] ) from SUBSET_1:sch 3();
hence ex b₁ being Subset-Family of st
for A being Subset of holds
( A in b₁ iff ex B being Subset of st
( B in G & A = f " B ) ) ; :: thesis: verum