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