now :: thesis: ex a being set st
for b being set holds
( P1[a] or P2[b] )
A2: now :: thesis: ( ( for b being set holds P2[b] ) implies ex a being set st
for b being set holds
( P1[a] or P2[b] ) )
set a = the set ;
assume for b being set holds P2[b] ; :: thesis: ex a being set st
for b being set holds
( P1[a] or P2[b] )
then for b being set holds
( P1[ the set ] or P2[b] ) ;
hence ex a being set st
for b being set holds
( P1[a] or P2[b] ) ; :: thesis: verum
end;
now :: thesis: ( ex a being set st P1[a] implies ex a being set st
for b being set holds
( P1[a] or P2[b] ) )
given a being set such that A3: P1[a] ; :: thesis: ex a being set st
for b being set holds
( P1[a] or P2[b] )
for b being set holds
( P1[a] or P2[b] ) by A3;
hence ex a being set st
for b being set holds
( P1[a] or P2[b] ) ; :: thesis: verum
end;
hence ex a being set st
for b being set holds
( P1[a] or P2[b] ) by A1, A2; :: thesis: verum
end;
hence ex a being set st
for b being set holds
( P1[a] or P2[b] ) ; :: thesis: verum