now

A2: now

consider a being set ;
assume for b being set holds P₂[b] ; :: thesis: ex a being set st
for b being set holds
( P₁[a] or P₂[b] )
then for b being set holds
( P₁[a] or P₂[b] ) ;
hence ex a being set st
for b being set holds
( P₁[a] or P₂[b] ) ; :: thesis: verum

end;

now

given a being set such that A3: P₁[a] ; :: thesis: ex a being set st
for b being set holds
( P₁[a] or P₂[b] )
for b being set holds
( P₁[a] or P₂[b] ) by A3;
hence ex a being set st
for b being set holds
( P₁[a] or P₂[b] ) ; :: thesis: verum

end;

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

end;

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