:: deftheorem Def2 defines ConwayDay CGAMES_1:def 2 :
for alpha being Ordinal
for b₂ being set holds
( b₂ = ConwayDay alpha iff ex f being Sequence st
( alpha in dom f & f . alpha = b₂ & ( for beta being Ordinal st beta in dom f holds
f . beta = { left-right(# x,y #) where x, y is Subset of (union (rng (f | beta))) : verum } ) ) );