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