:: deftheorem defines PQSub SUBSTUT1:def 14 :
for A being QC-alphabet
for p being QC-formula of A
for Sub being CQC_Substitution of A
for b being object holds
( p,Sub PQSub b iff ( ( p is universal implies b = ExpandSub ((bound_in p),(the_scope_of p),(RestrictSub ((bound_in p),p,Sub))) ) & ( not p is universal implies b = {} ) ) );