defpred S₁[ object ] means ex i being Nat ex p being Element of CQC-WFF Al 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 object holds
( a in X iff ( a in bound_QC-variables Al & S₁[a] ) ) from XBOOLE_0:sch 1();
take X ; :: thesis: ( X is Subset of (bound_QC-variables Al) & ( for a being object holds
( a in X iff ex i being Nat ex p being Element of CQC-WFF Al st
( i in dom f & p = f . i & a in still_not-bound_in p ) ) ) )
for a being object st a in X holds
a in bound_QC-variables Al by A1;
hence X is Subset of (bound_QC-variables Al) by TARSKI:def 3; :: thesis: for a being object holds
( a in X iff ex i being Nat ex p being Element of CQC-WFF Al st
( i in dom f & p = f . i & a in still_not-bound_in p ) )
thus for a being object holds
( a in X iff ex i being Nat ex p being Element of CQC-WFF Al st
( i in dom f & p = f . i & a in still_not-bound_in p ) ) by A1; :: thesis: verum