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