for x being set
for alpha being Ordinal
for g being ConwayGame st g in ConwayDay alpha & ( x in the_LeftOptions_of g or x in the_RightOptions_of g ) holds
x in ConwayDay alpha