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