let x be set ; :: thesis: for g being ConwayGame st ( x in the_LeftOptions_of g or x in the_RightOptions_of g ) holds
x is ConwayGame-like left-right
let g be ConwayGame; :: thesis: ( ( x in the_LeftOptions_of g or x in the_RightOptions_of g ) implies x is ConwayGame-like left-right )
assume ( x in the_LeftOptions_of g or x in the_RightOptions_of g ) ; :: thesis: x is ConwayGame-like left-right
then x in the_Options_of g by XBOOLE_0:def 3;
hence x is ConwayGame-like left-right by Th17; :: thesis: verum