let A be QC-alphabet ; for x being bound_QC-variable of A
for p being Element of QC-WFF A
for V being non empty Subset of (QC-variables A) holds Vars ((Ex (x,p)),V) = Vars (p,V)
let x be bound_QC-variable of A; for p being Element of QC-WFF A
for V being non empty Subset of (QC-variables A) holds Vars ((Ex (x,p)),V) = Vars (p,V)
let p be Element of QC-WFF A; for V being non empty Subset of (QC-variables A) holds Vars ((Ex (x,p)),V) = Vars (p,V)
let V be non empty Subset of (QC-variables A); 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 Th39
.=
Vars (('not' p),V)
by Th44
.=
Vars (p,V)
by Th39
;
verum