let g, gO be ConwayGame; :: thesis: ( gO in the_Options_of g implies ConwayRank gO in ConwayRank g )
set alpha = ConwayRank g;
A1: g in ConwayDay (ConwayRank g) by Def9;
assume gO in the_Options_of g ; :: thesis: ConwayRank gO in ConwayRank g
then consider beta being Ordinal such that
A2: ( beta in ConwayRank g & gO in ConwayDay beta ) by A1, Th9;
ConwayRank gO c= beta by A2, Th12;
hence ConwayRank gO in ConwayRank g by A2, ORDINAL1:12; :: thesis: verum