scheme :: CGAMES_1:sch 1
ConwayGameMinTot{ P₁[ ConwayGame] } :

ex g being ConwayGame st
( P₁[g] & ( for g1 being ConwayGame st ConwayRank g1 in ConwayRank g holds
not P₁[g1] ) )

provided

A1: ex g being ConwayGame st P₁[g]