:: deftheorem Def8 defines Bound_Vars SUBSTUT1:def 8 :
for A being QC-alphabet
for p being QC-formula of A
for b₃ being Subset of (bound_QC-variables A) holds
( b₃ = Bound_Vars p iff ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( b₃ = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of (bound_QC-variables A) holds
( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = Bound_Vars (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \/ {(bound_in p)} ) ) ) ) );