let g, gO be ConwayGame; ( not gO in the_Tree_of g or gO = g or ConwayRank gO in ConwayRank g )
assume
gO in the_Tree_of g
; ( 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;