theorem Th6: :: SURREALI:6

for n being Nat
for o being object
for Inv being Function holds
( (divL (o,Inv)) . (n + 1) = (((divL (o,Inv)) . n) \/ (divset (((divL (o,Inv)) . n),o,(R_ o),Inv))) \/ (divset (((divR (o,Inv)) . n),o,(L_ o),Inv)) & (divR (o,Inv)) . (n + 1) = (((divR (o,Inv)) . n) \/ (divset (((divL (o,Inv)) . n),o,(L_ o),Inv))) \/ (divset (((divR (o,Inv)) . n),o,(R_ o),Inv)) )