theorem Th25: :: SURREALN:25

for z being Surreal
for n being Nat holds
( ( 0_No <= z & z in Day n & not z == uDyadic . n implies ex x, y, p being Nat st
( z == uDyadic . (x + (y / (2 |^ p))) & y < 2 |^ p & x + p < n ) ) & ( for x, y, p being Nat st y < 2 |^ p & x + p < n holds
( 0_No <= uDyadic . (x + (y / (2 |^ p))) & uDyadic . (x + (y / (2 |^ p))) in Day n ) ) )