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