defpred S₁[ Ordinal] means ( $1 is natural implies P₁[$1] );
A3: S₁[ {} ] by A1;

A4: now

let A be Ordinal; :: thesis: ( S₁[A] implies S₁[ succ A] )
assume A5: S₁[A] ; :: thesis: S₁[ succ A]

now

assume succ A is natural ; :: thesis: S₁[ succ A]
then ( succ A in omega & A in succ A ) by ORDINAL1:10, ORDINAL1:def 13;
then A is Element of omega by ORDINAL1:19;
hence S₁[ succ A] by A2, A5; :: thesis: verum

end;

hence S₁[ succ A] ; :: thesis: verum

end;

A6: now

let A be Ordinal; :: thesis: ( A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S₁[B] ) implies S₁[A] )
A7: {} c= A ;
assume A <> {} ; :: thesis: ( A is limit_ordinal & ( for B being Ordinal st B in A holds
S₁[B] ) implies S₁[A] )
then {} c< A by A7, XBOOLE_0:def 8;
then A8: {} in A by ORDINAL1:21;
assume A is limit_ordinal ; :: thesis: ( ( for B being Ordinal st B in A holds
S₁[B] ) implies S₁[A] )
then ( omega c= A & not A in A ) by A8, ORDINAL1:def 12;
then not A in omega ;
hence ( ( for B being Ordinal st B in A holds
S₁[B] ) implies S₁[A] ) by ORDINAL1:def 13; :: thesis: verum

end;

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