:: deftheorem Def9 defines RSub1 SUBLEMMA:def 9 :
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for b₃ being set holds
( b₃ = RSub1 p iff for b being object holds
( b in b₃ iff ex x being bound_QC-variable of Al st
( x = b & not x in still_not-bound_in p ) ) );