for A being QC-alphabet
for p being Element of QC-WFF A
for V being non empty Subset of (QC-variables A) st p is atomic holds
( Vars (p,V) = variables_in ((the_arguments_of p),V) & Vars (p,V) = { ((the_arguments_of p) . k) where k is Nat : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in V ) } )