let x be object ; :: according to SURREAL0:def 16 :: thesis: ( not x in (unique_No_op A) . o or x is surreal )
assume A1: x in (unique_No_op A) . o ; :: thesis: x is surreal
then A2: o in dom (unique_No_op A) by FUNCT_1:def 2;
then A3: o in succ A by Def9;
reconsider o = o as Ordinal by A2;
(unique_No_op A) . o c= Day o by A3, Def9;
hence x is surreal by A1; :: thesis: verum