ex x being bound_QC-variable of A ex p being Element of QC-WFF A st F = All (x,p) by A1, Def21;
hence ex b₁ being QC-formula of A ex x being bound_QC-variable of A st F = All (x,b₁) ; :: thesis: verum