let g be ConwayGame; :: thesis: g in the_Tree_of g
ex f being ConwayGameChain st
( f . 1 = g & f . (len f) = g ) by Lm2;
hence g in the_Tree_of g by Def12; :: thesis: verum