let A be QC-alphabet ; for H being Element of QC-WFF A st H is existential holds
H = Ex ((bound_in (the_argument_of H)),(the_argument_of (the_scope_of (the_argument_of H))))
let H be Element of QC-WFF A; ( 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 of A, H1 being Element of QC-WFF A such that A1:
H = Ex (x,H1)
; QC_LANG2:def 13 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 Th1;
( the_argument_of ('not' (All (x,('not' H1)))) = All (x,('not' H1)) & the_scope_of (All (x,('not' H1))) = 'not' H1 )
by Th1, Th7;
hence
H = Ex ((bound_in (the_argument_of H)),(the_argument_of (the_scope_of (the_argument_of H))))
by A1, A2, Th7; verum