let x be set ; :: thesis: for g being ConwayGame holds
( x in the_Tree_of g iff ( x = g or ex gO being ConwayGame st
( gO in the_Options_of g & x in the_Tree_of gO ) ) )
let g be ConwayGame; :: thesis: ( x in the_Tree_of g iff ( x = g or ex gO being ConwayGame st
( gO in the_Options_of g & x in the_Tree_of gO ) ) )

hereby :: thesis: ( ( x = g or ex gO being ConwayGame st
( gO in the_Options_of g & x in the_Tree_of gO ) ) implies x in the_Tree_of g )

assume x in the_Tree_of g ; :: thesis: ( x <> g implies ex gO being set st
( gO in the_Options_of g & x in the_Tree_of gO ) )
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: ex gO being set st
( gO in the_Options_of g & x in the_Tree_of gO )
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: ( gO in the_Options_of g & x in the_Tree_of gO )
thus gO in the_Options_of g by Def11, A3, A1; :: thesis: x in the_Tree_of gO
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: verum

end;

hereby :: thesis: verum

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

per cases ( x = g or ex gO being ConwayGame st
( gO in the_Options_of g & x in the_Tree_of gO ) ) by A4;

suppose x = g ; :: thesis: x in the_Tree_of g

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

end;

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

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 ) by A5, A6;
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: verum

end;

end;

end;