theorem Th38: :: SURREALN:38

for i being Integer
for p being Nat
for x being Surreal holds
( [{(uDyadic . (i / (2 |^ p)))},{(uDyadic . ((i + 2) / (2 |^ p)))}] is Surreal & ( x = [{(uDyadic . (i / (2 |^ p)))},{(uDyadic . ((i + 2) / (2 |^ p)))}] implies x == uDyadic . ((i + 1) / (2 |^ p)) ) )