A1: {0_No} << {} ;
set b = born 0_No;
A2: 0_No in Day (born 0_No) by SURREAL0:def 18;
for o being object st o in {0_No} \/ {} holds
ex O being Ordinal st
( O in succ (born 0_No) & o in Day O )

proof

let o be object ; :: thesis: ( o in {0_No} \/ {} implies ex O being Ordinal st
( O in succ (born 0_No) & o in Day O ) )
assume o in {0_No} \/ {} ; :: thesis: ex O being Ordinal st
( O in succ (born 0_No) & o in Day O )
then o = 0_No by TARSKI:def 1;
hence ex O being Ordinal st
( O in succ (born 0_No) & o in Day O ) by A2, ORDINAL1:6; :: thesis: verum

end;

then [{0_No},{}] in Day (succ (born 0_No)) by A1, SURREAL0:46;
hence [{0_No},{}] is Surreal ; :: thesis: verum