defpred S1[ Ordinal] means ( $1 is natural implies P1[$1] );
A3: now :: thesis: for A being Ordinal st S1[A] holds
S1[ succ A]
let A be Ordinal; :: thesis: ( S1[A] implies S1[ succ A] )
assume A4: S1[A] ; :: thesis: S1[ succ A]
now :: thesis: ( succ A is natural implies S1[ succ A] )
assume succ A is natural ; :: thesis: S1[ succ A]
then A5: succ A in omega ;
A in succ A by ORDINAL1:6;
then A is Element of omega by A5, ORDINAL1:10;
hence S1[ succ A] by A2, A4; :: thesis: verum
end;
hence S1[ succ A] ; :: thesis: verum
end;
A6: now :: thesis: for A being Ordinal st A <> 0 & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
let A be Ordinal; :: thesis: ( A <> 0 & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume A7: A <> 0 ; :: thesis: ( A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
0 c= A ;
then 0 c< A by A7;
then A8: 0 in A by ORDINAL1:11;
A9: not A in A ;
assume A is limit_ordinal ; :: thesis: ( ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
then omega c= A by A8, ORDINAL1:def 11;
then not A in omega by A9;
hence ( ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] ) by ORDINAL1:def 12; :: thesis: verum
end;
A10: S1[ 0 ] by A1;
for A being Ordinal holds S1[A] from ORDINAL2:sch 1(A10, A3, A6);
 hence P1[F1()] ; :: thesis: verum