let g, gO be ConwayGame; :: thesis: ( gO in the_Tree_of g implies ConwayRank gO c= ConwayRank g )
assume A1: gO in the_Tree_of g ; :: thesis: ConwayRank gO c= ConwayRank g

per cases ( gO = g or ConwayRank gO in ConwayRank g ) by A1, Th28;

suppose gO = g ; :: thesis: ConwayRank gO c= ConwayRank g

hence ConwayRank gO c= ConwayRank g ; :: thesis: verum

end;

suppose ConwayRank gO in ConwayRank g ; :: thesis: ConwayRank gO c= ConwayRank g

hence ConwayRank gO c= ConwayRank g by ORDINAL1:def 2; :: thesis: verum

end;

end;