let x be Surreal; :: thesis: ( x is positive implies ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} c= Positives (born x) )
assume A1: x is positive ; :: thesis: ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} c= Positives (born x)
then A2: ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} c= (L_ x) \/ (R_ x) by Th20;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} or a in Positives (born x) )
assume A3: a in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} ; :: thesis: a in Positives (born x)
then reconsider a = a as Surreal by SURREAL0:def 16;
A4: a is positive by A1, A3, Th21;
born a in born x by A3, A2, SURREALO:1;
then ( a in Day (born a) & Day (born a) c= Day (born x) ) by SURREAL0:35, SURREAL0:def 18, ORDINAL1:def 2;
hence a in Positives (born x) by A4, Def10; :: thesis: verum