let g, gO be ConwayGame; :: thesis: ( not gO in the_Tree_of g or gO = g or ConwayRank gO in ConwayRank g )
assume gO in the_Tree_of g ; :: thesis: ( gO = g or ConwayRank gO in ConwayRank g )
then consider f being ConwayGameChain such that
A1: ( f . 1 = gO & f . (len f) = g ) by Def12;
reconsider n = 1 as Element of dom f by FINSEQ_5:6;
reconsider m = len f as Element of dom f by FINSEQ_5:6;
A2: m >= 1 by NAT_1:14;

per cases ( m = 1 or m > 1 ) by A2, XXREAL_0:1;

suppose m = 1 ; :: thesis: ( gO = g or ConwayRank gO in ConwayRank g )

hence ( gO = g or ConwayRank gO in ConwayRank g ) by A1; :: thesis: verum

end;

suppose m > 1 ; :: thesis: ( gO = g or ConwayRank gO in ConwayRank g )

then ConwayRank (f . n) in ConwayRank (f . m) by Th21;
hence ( gO = g or ConwayRank gO in ConwayRank g ) by A1; :: thesis: verum

end;

end;