scheme :: ORDINAL1:sch 2
TransfiniteInd{ P₁[ Ordinal] } :

for A being Ordinal holds P₁[A]

provided

A1: for A being Ordinal st ( for C being Ordinal st C in A holds
P₁[C] ) holds
P₁[A]