let x be set ; :: thesis: 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
let alpha be Ordinal; :: thesis: 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
let g be ConwayGame; :: thesis: ( g in ConwayDay alpha & ( x in the_LeftOptions_of g or x in the_RightOptions_of g ) implies x in ConwayDay alpha )
( ( x in the_LeftOptions_of g or x in the_RightOptions_of g ) implies x in the_Options_of g ) by XBOOLE_0:def 3;
hence ( g in ConwayDay alpha & ( x in the_LeftOptions_of g or x in the_RightOptions_of g ) implies x in ConwayDay alpha ) by Th10; :: thesis: verum