let g1 be Element of the_Tree_of g; :: thesis: g1 is ConwayGame-like
consider alpha being Ordinal such that
A1: g in ConwayDay alpha by Def3;
ex f being ConwayGameChain st
( f . 1 = g1 & f . (len f) = g ) by Def12;
then g1 in ConwayDay alpha by Th23, A1;
hence g1 is ConwayGame-like ; :: thesis: verum