defpred S2[ ConwayGame] means P1[$1];
assume A2: ex g being ConwayGame st S2[g] ; :: thesis: contradiction
ex g being ConwayGame st
( S2[g] & ( for gO being ConwayGame st gO in the_Options_of g holds
not S2[gO] ) ) from CGAMES_1:sch 2(A2);
 hence contradiction by A1; :: thesis: verum