assume A2: ( for a being set holds P1[a] or ex b being set st P2[b] ) ; :: thesis: contradiction
per cases ( ex b being set st P2[b] or for a being set holds P1[a] ) by A2;
suppose not for b being set holds P2[b] ; :: thesis: contradiction
then consider b being set such that
A3: P2[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
( P1[a] & P2[b] ) by A1;
hence contradiction by A3; :: thesis: verum
end;
hence contradiction ; :: thesis: verum
end;
suppose A4: for a being set holds P1[a] ; :: thesis: contradiction
now :: thesis: for b being set holds contradiction
let b be set ; :: thesis: contradiction
ex a being set st
( P1[a] & P2[b] ) by A1;
hence contradiction by A4; :: thesis: verum
end;
hence contradiction ; :: thesis: verum
end;
end;