let p be Element of QC-WFF ; :: thesis: for V being non empty Subset of QC-variables 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; :: thesis: ( 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 ; :: thesis: 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 Th50
.= Vars (('not' (the_argument_of (the_scope_of (the_argument_of p)))),V) by Th55
.= Vars ((the_argument_of (the_scope_of (the_argument_of p))),V) by Th50 ;
hence Vars (p,V) = Vars ((the_argument_of (the_scope_of (the_argument_of p))),V) ; :: thesis: verum