:: deftheorem defines QSub SUBSTUT1:def 15 :
for A being QC-alphabet
for b₂ being Function holds
( b₂ = QSub A iff for a being object holds
( a in b₂ iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being object st
( a = [[p,Sub],b] & p,Sub PQSub b ) ) );