:: deftheorem defines nonnegative CGAMES_1:def 15 :
for g being ConwayGame holds
( g is nonnegative iff ex s being set st
( g in s & ( for g1 being ConwayGame st g1 in s holds
for gR being ConwayGame st gR in the_RightOptions_of g1 holds
ex gRL being ConwayGame st
( gRL in the_LeftOptions_of gR & gRL in s ) ) ) );