defpred S₁[ Ordinal] means ( $1 is Ordinal of F₁() implies P₁[$1] );
A4: S₁[ {} ] by A1, ORDINAL4:35;
A5: for A being Ordinal st S₁[A] holds
S₁[ succ A]

proof

let A be Ordinal; :: thesis: ( S₁[A] implies S₁[ succ A] )
assume that
A6: ( A is Ordinal of F₁() implies P₁[A] ) and
A7: succ A is Ordinal of F₁() ; :: thesis: P₁[ succ A]
( A in succ A & succ A in On F₁() ) by A7, Th8, ORDINAL1:10;
then A in On F₁() by ORDINAL1:19;
then reconsider a = A as Ordinal of F₁() by Th8;
P₁[ succ a] by A2, A6;
hence P₁[ succ A] ; :: thesis: verum

end;

A8: for A being Ordinal st A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S₁[B] ) holds
S₁[A]

proof

let A be Ordinal; :: thesis: ( A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S₁[B] ) implies S₁[A] )
assume that
A9: ( A <> {} & A is limit_ordinal ) and
A10: for B being Ordinal st B in A & B is Ordinal of F₁() holds
P₁[B] ; :: thesis: S₁[A]
assume A is Ordinal of F₁() ; :: thesis: P₁[A]
then reconsider a = A as Ordinal of F₁() ;
( {} = 0-element_of F₁() & ( for b being Ordinal of F₁() st b in a holds
P₁[b] ) ) by A10, ORDINAL4:35;
hence P₁[A] by A3, A9; :: thesis: verum

end;

for A being Ordinal holds S₁[A] from ORDINAL2:sch 1(A4, A5, A8);
hence for a being Ordinal of F₁() holds P₁[a] ; :: thesis: verum