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

A2: now :: thesis: ( ( for b being set holds P₂[b] ) implies ex a being set st
for b being set holds
( P₁[a] or P₂[b] ) )

set a = the 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₁[ the set ] or P₂[b] ) ;
hence ex a being set st
for b being set holds
( P₁[a] or P₂[b] ) ; :: thesis: verum

end;

now :: thesis: ( ex a being set st P₁[a] implies ex a being set st
for b being set holds
( P₁[a] or P₂[b] ) )

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