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