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