let p be Element of QC-WFF ; :: thesis: for V being non empty Subset of QC-variables st p is disjunctive holds
Vars p,V = (Vars (the_left_disjunct_of p),V) \/ (Vars (the_right_disjunct_of p),V)
let V be non empty Subset of QC-variables ; :: thesis: ( p is disjunctive implies Vars p,V = (Vars (the_left_disjunct_of p),V) \/ (Vars (the_right_disjunct_of p),V) )
set p1 = the_left_disjunct_of p;
set p2 = the_right_disjunct_of p;
assume p is disjunctive ; :: thesis: Vars p,V = (Vars (the_left_disjunct_of p),V) \/ (Vars (the_right_disjunct_of p),V)
then p = (the_left_disjunct_of p) 'or' (the_right_disjunct_of p) by QC_LANG2:53;
then p = 'not' (('not' (the_left_disjunct_of p)) '&' ('not' (the_right_disjunct_of p))) by QC_LANG2:def 3;
hence Vars p,V = Vars (('not' (the_left_disjunct_of p)) '&' ('not' (the_right_disjunct_of p))),V by Th50
.= (Vars ('not' (the_left_disjunct_of p)),V) \/ (Vars ('not' (the_right_disjunct_of p)),V) by Th53
.= (Vars (the_left_disjunct_of p),V) \/ (Vars ('not' (the_right_disjunct_of p)),V) by Th50
.= (Vars (the_left_disjunct_of p),V) \/ (Vars (the_right_disjunct_of p),V) by Th50 ;
:: thesis: verum