let x be set ; :: thesis: for alpha being Ordinal
for g being ConwayGame st g in ConwayDay alpha & x in the_Options_of g holds
x in ConwayDay alpha
let alpha be Ordinal; :: thesis: for g being ConwayGame st g in ConwayDay alpha & x in the_Options_of g holds
x in ConwayDay alpha
let g be ConwayGame; :: thesis: ( g in ConwayDay alpha & x in the_Options_of g implies x in ConwayDay alpha )
assume ( g in ConwayDay alpha & x in the_Options_of g ) ; :: thesis: x in ConwayDay alpha
then consider beta being Ordinal such that
A1: ( beta in alpha & x in ConwayDay beta ) by Th9;
beta c= alpha by A1, ORDINAL1:def 2;
then ConwayDay beta c= ConwayDay alpha by Th3;
hence x in ConwayDay alpha by A1; :: thesis: verum