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 :: thesis: for d being set holds not d = b

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 :: thesis: for b being set holds contradiction

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

end;

hence contradiction ; :: thesis: verum

end;

end;