ex p, q being Element of QC-WFF st F = p '&' q by A1, Def19;
hence ex b₁ being QC-formula ex p being Element of QC-WFF st F = p '&' b₁ ; :: thesis: verum