:: deftheorem Def10 defines RSub2 SUBLEMMA:def 10 :
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for Sub being CQC_Substitution of Al
for b₄ being set holds
( b₄ = RSub2 (p,Sub) iff for b being object holds
( b in b₄ iff ex x being bound_QC-variable of Al st
( x = b & x in still_not-bound_in p & x = (@ Sub) . x ) ) );