assume A2: for a being set holds P₁[a] ; :: thesis: P₂[]

now

let a be set ; :: thesis: P₂[]
P₁[a] by A2;
hence P₂[] by A1; :: thesis: verum

end;

hence P₂[] ; :: thesis: verum