consider b being set ;
ex a being set st P₁[a,b] by A1;
hence ex a, b being set st P₁[a,b] ; :: thesis: verum