now :: thesis: for b being set ex b being set st
for a being set holds P₁[a,b]

let b be set ; :: thesis: ex b being set st
for a being set holds P₁[a,b]
for a being set holds P₁[a,b] by A1;
hence ex b being set st
for a being set holds P₁[a,b] ; :: thesis: verum

end;

hence ex b being set st
for a being set holds P₁[a,b] ; :: thesis: verum