defpred S₁[ set ] means ex i being Element of NAT ex p being Element of CQC-WFF st
( i in dom f & p = f . i & $1 in still_not-bound_in p );
consider X being set such that
A1: for a being set holds
( a in X iff ( a in bound_QC-variables & S₁[a] ) ) from XBOOLE_0:sch 1();
take X ; :: thesis: ( X is Subset of bound_QC-variables & ( for a being set holds
( a in X iff ex i being Element of NAT ex p being Element of CQC-WFF st
( i in dom f & p = f . i & a in still_not-bound_in p ) ) ) )
for a being set st a in X holds
a in bound_QC-variables by A1;
hence X is Subset of bound_QC-variables by TARSKI:def 3; :: thesis: for a being set holds
( a in X iff ex i being Element of NAT ex p being Element of CQC-WFF st
( i in dom f & p = f . i & a in still_not-bound_in p ) )
thus for a being set holds
( a in X iff ex i being Element of NAT ex p being Element of CQC-WFF st
( i in dom f & p = f . i & a in still_not-bound_in p ) ) by A1; :: thesis: verum