let H be Element of QC-WFF ; :: thesis: ( H is existential implies H = Ex (bound_in (the_argument_of H)),(the_argument_of (the_scope_of (the_argument_of H))) )
given x being bound_QC-variable, H1 being Element of QC-WFF such that A1: H = Ex x,H1 ; :: according to QC_LANG2:def 13 :: thesis: H = Ex (bound_in (the_argument_of H)),(the_argument_of (the_scope_of (the_argument_of H)))
A2: the_argument_of ('not' H1) = H1 by Th2;
( the_argument_of ('not' (All x,('not' H1))) = All x,('not' H1) & the_scope_of (All x,('not' H1)) = 'not' H1 ) by Th2, Th8;
hence H = Ex (bound_in (the_argument_of H)),(the_argument_of (the_scope_of (the_argument_of H))) by A1, A2, Th8; :: thesis: verum