defpred S2[ Ordinal] means ( P1[$1] & $1 in omega );
A6: ex A being Ordinal st S2[A] by A3, A5;
consider A being Ordinal such that
A7: S2[A] and
A8: for B being Ordinal st S2[B] holds
A c= B from ORDINAL1:sch 1(A6);
 A9: {} in A by A2, A4, A7, ORDINAL3:8;
now :: thesis: not A is limit_ordinal
assume A is limit_ordinal ; :: thesis: contradiction
then omega c= A by A9, ORDINAL1:def 11;
then A in A by A7;
hence contradiction ; :: thesis: verum
end;
then consider B being Ordinal such that
A10: A = succ B by ORDINAL1:29;
A11: B in A by A10, ORDINAL1:8;
then A12: B in omega by A7, ORDINAL1:10;
then reconsider s = B as ordinal Element of RAT+ by Lm6;
take s ; :: thesis: ( s in omega & P1[s] & P1[s + F2()] )
thus ( s in omega & P1[s] ) by A8, A11, A12, ORDINAL1:5; :: thesis: P1[s + F2()]
A = B +^ 1 by A10, ORDINAL2:31;
hence P1[s + F2()] by A1, A7, Th58; :: thesis: verum