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_Options_of g holds
not P₁[gO] ) )
thus P₁[g] by A2; :: thesis: for gO being ConwayGame st gO in the_Options_of g holds
not P₁[gO]
let gO be ConwayGame; :: thesis: ( gO in the_Options_of g implies not P₁[gO] )
assume gO in the_Options_of g ; :: thesis: P₁[gO]
then ConwayRank gO in ConwayRank g by Th14;
hence P₁[gO] by A2; :: thesis: verum