let x be Surreal; :: thesis: ( born x = {} iff x = 0_No )

hereby :: thesis: ( x = 0_No implies born x = {} )

assume born x = {} ; :: thesis: x = 0_No
then x in Day {} by Def18;
hence x = 0_No by Th2, TARSKI:def 1; :: thesis: verum

end;

assume x = 0_No ; :: thesis: born x = {}
then x in Games {} by Th2, TARSKI:def 1;
then x in Day {} by Th8;
then born x c= {} by Def18;
hence born x = {} ; :: thesis: verum