let g be ConwayGame; :: thesis: ConwayZero in the_Tree_of g
defpred S₂[ ConwayGame] means not ConwayZero in the_Tree_of $1;
assume not ConwayZero in the_Tree_of g ; :: thesis: contradiction
then A1: ex g being ConwayGame st S₂[g] ;
consider g being ConwayGame such that
A2: ( S₂[g] & ( for gO being ConwayGame st gO in the_Options_of g holds
not S₂[gO] ) ) from CGAMES_1:sch 2(A1);

per cases ( g = ConwayZero or the_Options_of g <> {} ) by Th6;

suppose g = ConwayZero ; :: thesis: contradiction

hence contradiction by Th24, A2; :: thesis: verum

end;

suppose the_Options_of g <> {} ; :: thesis: contradiction

then consider x being object such that
A3: x in the_Options_of g by XBOOLE_0:def 1;
reconsider gO = x as ConwayGame by Th17, A3;
A4: ConwayZero in the_Tree_of gO by A2, A3;
the_Options_of g c= the_Tree_of g by Th34;
then the_Tree_of gO c= the_Tree_of g by Th31, A3;
hence contradiction by A2, A4; :: thesis: verum

end;

end;