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