defpred S₁[ Ordinal] means ( {} in $1 & $1 is limit_ordinal );
A1: ex A being Ordinal st S₁[A] by Th32;
ex C being Ordinal st
( S₁[C] & ( for A being Ordinal st S₁[A] holds
C c= A ) ) from ORDINAL1:sch 1(A1);
hence ex b₁ being set st
( {} in b₁ & b₁ is limit_ordinal & b₁ is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds
b₁ c= A ) ) ; :: thesis: verum