:: deftheorem Def3 defines transitions_of SURREALS:def 3 :
for x0 being pair object
for x being object
for b₃ being Function holds
( b₃ = transitions_of (x0,x) iff ( dom b₃ = NAT & b₃ . 0 = x0 & ( for n being Nat holds
( b₃ . n is pair & (b₃ . (n + 1)) `1 = (L_ (b<sub>3</sub> . n)) \/ (sqrt (x,(L_ (b<sub>3</sub> . n)),(R_ (b<sub>3</sub> . n)))) & (b<sub>3</sub> . (n + 1)) `2 = ((R_ (b₃ . n)) \/ (sqrt (x,(L_ (b₃ . n)),(L_ (b₃ . n))))) \/ (sqrt (x,(R_ (b₃ . n)),(R_ (b₃ . n)))) ) ) ) );