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;