consider g being ConwayGame such that
A2: ( P₁[g] & ( for g1 being ConwayGame st ConwayRank g1 in ConwayRank g holds
not P₁[g1] ) ) from CGAMES_1:sch 1(A1);
take g ; :: thesis: ( P₁[g] & ( for gO being ConwayGame st gO in the_proper_Tree_of g holds
not P₁[gO] ) )

now :: thesis: for gO being ConwayGame st gO in the_proper_Tree_of g holds
not P₁[gO]

let gO be ConwayGame; :: thesis: ( gO in the_proper_Tree_of g implies not P₁[gO] )
assume gO in the_proper_Tree_of g ; :: thesis: P₁[gO]
then ( gO in the_Tree_of g & gO <> g ) by ZFMISC_1:56;
then ConwayRank gO in ConwayRank g by Th28;
hence P₁[gO] by A2; :: thesis: verum

end;

hence ( P₁[g] & ( for gO being ConwayGame st gO in the_proper_Tree_of g holds
not P₁[gO] ) ) by A2; :: thesis: verum