let x be set ; :: thesis:
let g be ConwayGame; :: thesis:

hereby :: thesis:

assume x in the_Tree_of g ; :: thesis:
then consider f being ConwayGameChain such that
A1: ( f . 1 = x & f . (len f) = g ) by Def12;
reconsider n = len f as Element of dom f by FINSEQ_5:6;
assume A2: x <> g ; :: thesis:
then A3: n > 1 by A1, NAT_1:53;
reconsider n1 = n - 1 as Element of dom f by Th20, A1, A2, NAT_1:53;
take gO = f . n1; :: thesis:
thus gO in the_Options_of g by Def11, A3, A1; :: thesis:
not n1 is zero ;
then reconsider nf = f | n1 as ConwayGameChain by Th25;
( n1 < n & 1 in dom nf & len nf in dom nf ) by FINSEQ_5:6, XREAL_1:44;
then ( len nf = n1 & nf . 1 = f . 1 & nf . (len nf) = f . (len nf) ) by FINSEQ_1:59, FUNCT_1:47;
hence x in the_Tree_of gO by Def12, A1; :: thesis:

end;

hereby :: thesis:

assume A4: ( x = g or ex gO being ConwayGame st
( gO in the_Options_of g & x in the_Tree_of gO ) ) ; :: thesis:

per cases by A4;

suppose x = g ; :: thesis:

hence x in the_Tree_of g by Th24; :: thesis:

end;

suppose ex gO being ConwayGame st
( gO in the_Options_of g & x in the_Tree_of gO ) ; :: thesis:

then consider gO being ConwayGame such that
A5: ( gO in the_Options_of g & x in the_Tree_of gO ) ;
consider f being ConwayGameChain such that
A6: ( f . 1 = x & f . (len f) = gO ) by A5, Def12;
ex g1 being ConwayGame st
( g1 = <*g*> . 1 & f . (len f) in the_Options_of g1 )

proof

take g ; :: thesis:
thus ( g = <*g*> . 1 & f . (len f) in the_Options_of g ) by A5, A6, FINSEQ_1:def 8; :: thesis:

end;

then reconsider nf = f ^ <*g*> as ConwayGameChain by Th26;
( 1 in dom f & len nf = (len f) + 1 ) by FINSEQ_2:16, FINSEQ_5:6;
then ( nf . 1 = x & nf . (len nf) = g ) by A6, FINSEQ_1:42, FINSEQ_1:def 7;
hence x in the_Tree_of g by Def12; :: thesis:

end;

end;

end;