thus ( ex a being set st P₁[a] or for b being set holds P₂[b] ) by A1; :: thesis: verum