for alpha being Ordinal
for g being ConwayGame holds
( ConwayRank g in alpha iff ex beta being Ordinal st
( beta in alpha & g in ConwayDay beta ) )