defpred S₁[ Ordinal] means ( $1 is natural implies P₁[$1] );

A3: now

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

now

assume succ A is natural ; :: thesis: S₁[ succ A]
then A5: succ A in omega by ORDINAL1:def 12;
A in succ A by ORDINAL1:6;
then A is Element of omega by A5, ORDINAL1:10;
hence S₁[ succ A] by A2, A4; :: 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] )
assume A7: A <> {} ; :: thesis: ( A is limit_ordinal & ( for B being Ordinal st B in A holds
S₁[B] ) implies S₁[A] )
{} c= A ;
then {} c< A by A7, XBOOLE_0:def 8;
then A8: {} 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
S₁[B] ) implies S₁[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
S₁[B] ) implies S₁[A] ) by ORDINAL1:def 12; :: thesis: verum

end;

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