:: deftheorem Def9 defines ConwayRank CGAMES_1:def 9 :
for g being set st g is ConwayGame holds
for b₂ being Ordinal holds
( b₂ = ConwayRank g iff ( g in ConwayDay b₂ & ( for beta being Ordinal st beta in b₂ holds
not g in ConwayDay beta ) ) );