defpred S₁[ Ordinal] means X c= Rank $1;
A1: ex A being Ordinal st S₁[A] by Th69;
thus ex A being Ordinal st
( S₁[A] & ( for B being Ordinal st S₁[B] holds
A c= B ) ) from ORDINAL1:sch 1(A1); :: thesis: verum