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)
( p => q is conditional & the_antecedent_of (p => q) = p & the_consequent_of (p => q) = q ) by QC_LANG2:46, QC_LANG2:def 11;
hence Vars (p => q),V = (Vars p,V) \/ (Vars q,V) by Th58; :: thesis: verum