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:10;

now

assume A is limit_ordinal ; :: thesis: contradiction
then omega c= A by A9, ORDINAL1:def 12;
then A in A by A7;
hence contradiction ; :: thesis: verum

end;

then consider B being Ordinal such that
A10: A = succ B by ORDINAL1:42;
B in A by A10, ORDINAL1:13;
then A11: ( B in omega & not A c= B ) by A7, ORDINAL1:7, ORDINAL1:19;
then reconsider s = B as ordinal Element of RAT+ by Lm5;
take s ; :: thesis: ( s in omega & P₁[s] & P₁[s + F₂()] )
thus ( s in omega & P₁[s] ) by A8, A11; :: thesis: P₁[s + F₂()]
A = B +^ 1 by A10, ORDINAL2:48;
hence P₁[s + F₂()] by A1, A7, Th64; :: thesis: verum