thus ex R being Subset-Family of S st
for A being Subset of S holds
( A in R iff ex B being Subset of T st
( B in G & A = f .: B ) ) :: thesis: verum

proof

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

end;