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