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