the_Tree_of g c= ConwayDay alpha

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in the_Tree_of g or z in ConwayDay alpha )
assume z in the_Tree_of g ; :: thesis: z in ConwayDay alpha
then consider f being ConwayGameChain such that
A1: ( f . 1 = z & f . (len f) = g ) by Def12;
thus z in ConwayDay alpha by A1, Th23; :: thesis: verum

end;

hence the_Tree_of g is Subset of (ConwayDay alpha) ; :: thesis: verum