defpred S₁[ set ] means $1 /\ X in G;
consider I being set such that
A1: for x being set holds
( x in I iff ( x in bool Omega & S₁[x] ) ) from XFAMILY:sch 1();
for x being object st x in I holds
x in bool Omega by A1;
then reconsider I = I as Subset-Family of Omega by TARSKI:def 3;
take I ; :: thesis: for A being Subset of Omega holds
( A in I iff A /\ X in G )
let A be Subset of Omega; :: thesis: ( A in I iff A /\ X in G )
thus ( A in I iff A /\ X in G ) by A1; :: thesis: verum