consider g being ConwayGame such that
A2: ( P1[g] & ( for g1 being ConwayGame st ConwayRank g1 in ConwayRank g holds
not P1[g1] ) ) from CGAMES_1:sch 1(A1);
 take g ; :: thesis: ( P1[g] & ( for gO being ConwayGame st gO in the_proper_Tree_of g holds
not P1[gO] ) )
now :: thesis: for gO being ConwayGame st gO in the_proper_Tree_of g holds
not P1[gO]
let gO be ConwayGame; :: thesis: ( gO in the_proper_Tree_of g implies not P1[gO] )
assume gO in the_proper_Tree_of g ; :: thesis: P1[gO]
then ( gO in the_Tree_of g & gO <> g ) by ZFMISC_1:56;
then ConwayRank gO in ConwayRank g by Th28;
hence P1[gO] by A2; :: thesis: verum
end;
hence ( P1[g] & ( for gO being ConwayGame st gO in the_proper_Tree_of g holds
not P1[gO] ) ) by A2; :: thesis: verum