defpred S₁[ Ordinal] means o in Day (R,$1);
A2: ex O being Ordinal st S₁[O] by A1;
ex A being Ordinal st
( S₁[A] & ( for B being Ordinal st S₁[B] holds
A c= B ) ) from ORDINAL1:sch 1(A2);
hence ex b₁ being Ordinal st
( o in Day (R,b₁) & ( for O being Ordinal st o in Day (R,O) holds
b₁ c= O ) ) ; :: thesis: verum