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