let A be QC-alphabet ; :: thesis: for p being Element of QC-WFF A
for V being non empty Subset of (QC-variables A) st p is conditional holds
Vars (p,V) = (Vars ((the_antecedent_of p),V)) \/ (Vars ((the_consequent_of p),V))
let p be Element of QC-WFF A; :: thesis: for V being non empty Subset of (QC-variables A) st p is conditional holds
Vars (p,V) = (Vars ((the_antecedent_of p),V)) \/ (Vars ((the_consequent_of p),V))
let V be non empty Subset of (QC-variables A); :: thesis: ( p is conditional implies Vars (p,V) = (Vars ((the_antecedent_of p),V)) \/ (Vars ((the_consequent_of p),V)) )
set p1 = the_antecedent_of p;
set p2 = the_consequent_of p;
assume p is conditional ; :: thesis: Vars (p,V) = (Vars ((the_antecedent_of p),V)) \/ (Vars ((the_consequent_of p),V))
then p = (the_antecedent_of p) => (the_consequent_of p) by QC_LANG2:38;
then p = 'not' ((the_antecedent_of p) '&' ('not' (the_consequent_of p))) by QC_LANG2:def 2;
hence Vars (p,V) = Vars (((the_antecedent_of p) '&' ('not' (the_consequent_of p))),V) by Th39
.= (Vars ((the_antecedent_of p),V)) \/ (Vars (('not' (the_consequent_of p)),V)) by Th42
.= (Vars ((the_antecedent_of p),V)) \/ (Vars ((the_consequent_of p),V)) by Th39 ;
:: thesis: verum