thus ex G being Subset-Family of (T | P) st
for Q being Subset of (T | P) holds
( Q in G iff ex R being Subset of T st
( R in F & R /\ P = Q ) ) :: thesis: verum
proof
defpred S1[ Subset of (T | P)] means ex R being Subset of T st
( R in F & R /\ P = $1 );
ex G being Subset-Family of (T | P) st
for Q being Subset of (T | P) holds
( Q in G iff S1[Q] ) from SUBSET_1:sch 3();
 hence ex G being Subset-Family of (T | P) st
for Q being Subset of (T | P) holds
( Q in G iff ex R being Subset of T st
( R in F & R /\ P = Q ) ) ; :: thesis: verum
end;