thus ex G being Subset-Family of st
for Q being Subset of holds
( Q in G iff ex R being Subset of st
( R in F & R /\ P = Q ) ) :: thesis: verum

proof

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

end;