theorem Th45: :: QC_LANG3:45

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 disjunctive holds
Vars (p,V) = (Vars ((the_left_disjunct_of p),V)) \/ (Vars ((the_right_disjunct_of p),V))