:: deftheorem Def5 defines BeforeGames SURREAL0:def 5 :
for A being Ordinal
for b₂ being Subset of (Games A) holds
( b₂ = BeforeGames A iff for a being object holds
( a in b₂ iff ex O being Ordinal st
( O in A & a in Games O ) ) );