let H be Element of QC-WFF ; :: 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, H1 being Element of QC-WFF 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 )
( 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 ) by A1, Th2, Th8;
hence ( H is negative & the_argument_of H is universal & the_scope_of (the_argument_of H) is negative ) by QC_LANG1:def 18, QC_LANG1:def 20; :: thesis: verum