defpred S₂[ Ordinal] means ( P₁[$1] & $1 in omega );
A6: ex A being Ordinal st S₂[A] by A3, A5;
consider A being Ordinal such that
A7: S₂[A] and
A8: for B being Ordinal st S₂[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 & P₁[s] & P₁[s + F₂()] )
thus ( s in omega & P₁[s] ) by A8, A11, A12, ORDINAL1:5; :: thesis: P₁[s + F₂()]
A = B +^ 1 by A10, ORDINAL2:31;
hence P₁[s + F₂()] by A1, A7, Th58; :: thesis: verum