consider y being Surreal such that
A1: ( born y = born_eq x & y == x ) by Def5;
y in Day (born y) by SURREAL0:def 18;
hence not born_eq_set x is empty by A1, Def6; :: thesis: verum