let g be ConwayGame; :: thesis: the_Options_of g c= the_proper_Tree_of g
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the_Options_of g or x in the_proper_Tree_of g )
assume A1: x in the_Options_of g ; :: thesis: x in the_proper_Tree_of g
reconsider gO = x as ConwayGame by A1, Th17;
gO in the_Tree_of gO by Th24;
then gO in the_Tree_of g by A1, Th27;
then ( gO = g or gO in the_proper_Tree_of g ) by ZFMISC_1:56;
hence x in the_proper_Tree_of g by A1, Th16; :: thesis: verum