let g be ConwayGame; :: thesis: ConwayZero in the_Tree_of g
defpred S2[ 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 S2[g] ;
consider g being ConwayGame such that
A2: ( S2[g] & ( for gO being ConwayGame st gO in the_Options_of g holds
not S2[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;