A2: ( ex a being set st P₁[a] or for b being set holds P₂[b] ) by A1;
ex a being set st
for b being set holds
( P₁[a] or P₂[b] ) from SCHEMS_1:sch 6(A2);
hence ex a being set st
for b being set holds
( P₁[a] or P₂[b] ) ; :: thesis: verum