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

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