P<=>Ax(P1(x)=>P1(x))?
.