let A be QC-alphabet ; for p being Element of QC-WFF A
for V being non empty Subset of (QC-variables A) st p is existential holds
Vars (p,V) = Vars ((the_argument_of (the_scope_of (the_argument_of p))),V)
let p be Element of QC-WFF A; for V being non empty Subset of (QC-variables A) st p is existential holds
Vars (p,V) = Vars ((the_argument_of (the_scope_of (the_argument_of p))),V)
let V be non empty Subset of (QC-variables A); ( p is existential implies Vars (p,V) = Vars ((the_argument_of (the_scope_of (the_argument_of p))),V) )
set p1 = the_argument_of (the_scope_of (the_argument_of p));
set x = bound_in (the_argument_of p);
assume
p is existential
; Vars (p,V) = Vars ((the_argument_of (the_scope_of (the_argument_of p))),V)
then
p = Ex ((bound_in (the_argument_of p)),(the_argument_of (the_scope_of (the_argument_of p))))
by QC_LANG2:40;
then
p = 'not' (All ((bound_in (the_argument_of p)),('not' (the_argument_of (the_scope_of (the_argument_of p))))))
by QC_LANG2:def 5;
then Vars (p,V) =
Vars ((All ((bound_in (the_argument_of p)),('not' (the_argument_of (the_scope_of (the_argument_of p)))))),V)
by Th39
.=
Vars (('not' (the_argument_of (the_scope_of (the_argument_of p)))),V)
by Th44
.=
Vars ((the_argument_of (the_scope_of (the_argument_of p))),V)
by Th39
;
hence
Vars (p,V) = Vars ((the_argument_of (the_scope_of (the_argument_of p))),V)
; verum