let p, q be Element of QC-WFF ; :: thesis: for V being non empty Subset of QC-variables holds Vars (p 'or' q),V = (Vars p,V) \/ (Vars q,V)
let V be non empty Subset of QC-variables ; :: thesis: Vars (p 'or' q),V = (Vars p,V) \/ (Vars q,V)
A1: the_right_disjunct_of (p 'or' q) = q by QC_LANG2:45;
( p 'or' q is disjunctive & the_left_disjunct_of (p 'or' q) = p ) by QC_LANG2:45, QC_LANG2:def 10;
hence Vars (p 'or' q),V = (Vars p,V) \/ (Vars q,V) by A1, Th56; :: thesis: verum