for A being Ordinal holds P₁[A]

A1: P₁[ 0 ] and
A2: for A being Ordinal st P₁[A] holds
P₁[ succ A] and
A3: for A being Ordinal st A <> 0 & A is limit_ordinal & ( for B being Ordinal st B in A holds
P₁[B] ) holds
P₁[A]