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 S1[ 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 S1[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;