defpred S_{1}[ 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_{1}[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

( 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

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