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 S₁[ 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 S₁[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;