for A being QC-alphabet
for x being bound_QC-variable of A
for H being Element of QC-WFF A holds the_argument_of (Ex (x,H)) = All (x,('not' H)) by Th1;