let A be QC-alphabet ; :: thesis: for H being Element of QC-WFF A st H is existential holds
( H is negative & the_argument_of H is universal & the_scope_of (the_argument_of H) is negative )
let H be Element of QC-WFF A; :: thesis: ( H is existential implies ( H is negative & the_argument_of H is universal & the_scope_of (the_argument_of H) is negative ) )
given x being bound_QC-variable of A, H1 being Element of QC-WFF A such that A1: H = Ex (x,H1) ; :: according to QC_LANG2:def 13 :: thesis: ( H is negative & the_argument_of H is universal & the_scope_of (the_argument_of H) is negative )
( 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 is negative & the_argument_of H is universal & the_scope_of (the_argument_of H) is negative ) by A1; :: thesis: verum