let x be set ; :: thesis: for g being ConwayGame st x in the_Options_of g holds
x is ConwayGame-like left-right
let g be ConwayGame; :: thesis: ( x in the_Options_of g implies x is ConwayGame-like left-right )
consider alpha being Ordinal such that
A1: g in ConwayDay alpha by Def3;
assume x in the_Options_of g ; :: thesis: x is ConwayGame-like left-right
then x in ConwayDay alpha by Th10, A1;
hence x is ConwayGame-like left-right by Th4; :: thesis: verum