let x be bound_QC-variable; :: thesis: for p being Element of QC-WFF
for V being non empty Subset of QC-variables holds Vars (Ex x,p),V = Vars p,V
let p be Element of QC-WFF ; :: thesis: for V being non empty Subset of QC-variables holds Vars (Ex x,p),V = Vars p,V
let V be non empty Subset of QC-variables ; :: thesis: Vars (Ex x,p),V = Vars p,V
Ex x,p = 'not' (All x,('not' p)) by QC_LANG2:def 5;
hence Vars (Ex x,p),V = Vars (All x,('not' p)),V by Th50
.= Vars ('not' p),V by Th55
.= Vars p,V by Th50 ;
:: thesis: verum