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 'or' 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 'or' q),V) = (Vars (p,V)) \/ (Vars (q,V))
let V be non empty Subset of (QC-variables A); :: thesis: Vars ((p 'or' q),V) = (Vars (p,V)) \/ (Vars (q,V))
A1: the_right_disjunct_of (p 'or' q) = q by QC_LANG2:29;
( p 'or' q is disjunctive & the_left_disjunct_of (p 'or' q) = p ) by QC_LANG2:29, QC_LANG2:def 10;
hence Vars ((p 'or' q),V) = (Vars (p,V)) \/ (Vars (q,V)) by A1, Th45; :: thesis: verum