:: deftheorem Def4 defines Games SURREAL0:def 4 :
for A being Ordinal
for b₂ being set holds
( b₂ = Games A iff ex L being Sequence st
( b₂ = L . A & dom L = succ A & ( for O being Ordinal st O in succ A holds
L . O = [:(bool (union (rng (L | O)))),(bool (union (rng (L | O)))):] ) ) );