scheme :: ORDINAL1:sch 2
TransfiniteInd{ P1[ Ordinal] } :
for A being Ordinal holds P1[A]
provided
A1: for A being Ordinal st ( for C being Ordinal st C in A holds
P1[C] ) holds
P1[A]