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