ex f being ConwayGameChain st
( f . 1 = g & f . (len f) = g ) by Lm2;
hence not the_Tree_of g is empty by Def12; :: thesis: verum