defpred S1[ Ordinal] means ( $1 is Ordinal of F1() implies P1[$1] );
A4: 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]
proof
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 that
A5: ( A <> 0 & A is limit_ordinal ) and
A6: for B being Ordinal st B in A & B is Ordinal of F1() holds
P1[B] ; :: thesis: S1[A]
assume A is Ordinal of F1() ; :: thesis: P1[A]
then reconsider a = A as Ordinal of F1() ;
( {} = 0-element_of F1() & ( for b being Ordinal of F1() st b in a holds
P1[b] ) ) by A6, ORDINAL4:33;
hence P1[A] by A3, A5; :: thesis: verum
end;
A7: for A being Ordinal st S1[A] holds
S1[ succ A]
proof
let A be Ordinal; :: thesis: ( S1[A] implies S1[ succ A] )
assume that
A8: ( A is Ordinal of F1() implies P1[A] ) and
A9: succ A is Ordinal of F1() ; :: thesis: P1[ succ A]
( A in succ A & succ A in On F1() ) by A9, ORDINAL1:6, ORDINAL1:def 9;
then A in On F1() by ORDINAL1:10;
then reconsider a = A as Ordinal of F1() by ORDINAL1:def 9;
P1[ succ a] by A2, A8;
hence P1[ succ A] ; :: thesis: verum
end;
A10: S1[ 0 ] by A1, ORDINAL4:33;
for A being Ordinal holds S1[A] from ORDINAL2:sch 1(A10, A7, A4);
 hence for a being Ordinal of F1() holds P1[a] ; :: thesis: verum