let p, q be Element of QC-WFF ; :: thesis: for V being non empty Subset of QC-variables holds Vars (p '&' q),V = (Vars p,V) \/ (Vars q,V)
let V be non empty Subset of QC-variables ; :: thesis: Vars (p '&' q),V = (Vars p,V) \/ (Vars q,V)
set pq = p '&' q;
A1: p '&' q is conjunctive by QC_LANG1:def 19;
then ( the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q ) by QC_LANG1:def 24, QC_LANG1:def 25;
hence Vars (p '&' q),V = (Vars p,V) \/ (Vars q,V) by A1, Lm2; :: thesis: verum