defpred S₁[ Ordinal] means x in Rank (succ $1);
reconsider x = x as set by TARSKI:1;
consider A being Ordinal such that
A1: x c= Rank A by Th62;
x in bool (Rank A) by A1;
then x in Rank (succ A) by Lm2;
then A2: ex A being Ordinal st S₁[A] ;
thus ex A being Ordinal st
( S₁[A] & ( for B being Ordinal st S₁[B] holds
A c= B ) ) from ORDINAL1:sch 1(A2); :: thesis: verum