let p be Element of QC-WFF ; :: thesis: for V being non empty Subset of QC-variables 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 ; :: 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:54;
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 Th50
.= (Vars (the_antecedent_of p),V) \/ (Vars ('not' (the_consequent_of p)),V) by Th53
.= (Vars (the_antecedent_of p),V) \/ (Vars (the_consequent_of p),V) by Th50 ;
:: thesis: verum