assume A2: ( for a being set holds P₁[a] or ex b being set st P₂[b] ) ; :: thesis: contradiction

per cases ( ex b being set st P₂[b] or for a being set holds P₁[a] ) by A2;

suppose not for b being set holds P₂[b] ; :: thesis: contradiction

then consider b being set such that
A3: P₂[b] ;

now

let d be set ; :: thesis: not d = b
assume d = b ; :: thesis: contradiction
ex a being set st
( P₁[a] & P₂[b] ) by A1;
hence contradiction by A3; :: thesis: verum

end;

hence contradiction ; :: thesis: verum

end;

suppose A4: for a being set holds P₁[a] ; :: thesis: contradiction

now

let b be set ; :: thesis: contradiction
consider a being set such that
A5: ( P₁[a] & P₂[b] ) by A1;
thus contradiction by A4, A5; :: thesis: verum

end;

hence contradiction ; :: thesis: verum

end;

end;