for a being Ordinal of F₁() holds P₁[a]

A1: P₁[ 0-element_of F₁()] and
A2: for a being Ordinal of F₁() st P₁[a] holds
P₁[ succ a] and
A3: for a being Ordinal of F₁() st a <> 0-element_of F₁() & a is limit_ordinal & ( for b being Ordinal of F₁() st b in a holds
P₁[b] ) holds
P₁[a]