(∀(x:A).(∀(y:A).R(y,x)→P(y))→P(x))→∀(x:A).P(x)\par(\forall(x:A).\;(\forall(y:A).\;R(y,x)\to P(y))\to P(x))\to\forall(x:A).\;% P(x)