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)))
( H = 'not' (All x,('not' H1)) & the_argument_of ('not' (All x,('not' H1))) = All x,('not' H1) & the_scope_of (All x,('not' H1)) = 'not' H1 & the_argument_of ('not' H1) = H1 & bound_in (All x,('not' H1)) = x ) by A1, Th2, Th8;
hence H = Ex (bound_in (the_argument_of H)),(the_argument_of (the_scope_of (the_argument_of H))) ; :: thesis: verum