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