set a = the set ;
P₁[ the set ] by A1;
hence ex a being set st P₁[a] ; :: thesis: verum