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:56;
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