let alpha be Ordinal; :: thesis:
let g be ConwayGame; :: thesis:

hereby :: thesis:

assume g in ConwayDay alpha ; :: thesis:
then consider w being strict left-right such that
A1: ( g = w & ( for x being set st x in the LeftOptions of w \/ the RightOptions of w holds
ex beta being Ordinal st
( beta in alpha & x in ConwayDay beta ) ) ) by Th1;
let x be set ; :: thesis:
A2: ( the LeftOptions of w = the_LeftOptions_of g & the RightOptions of w = the_RightOptions_of g ) by A1, Def6, Def7;
assume x in the_Options_of g ; :: thesis:
hence ex beta being Ordinal st
( beta in alpha & x in ConwayDay beta ) by A1, A2; :: thesis:

end;

hereby :: thesis:

assume A3: for x being set st x in the_Options_of g holds
ex beta being Ordinal st
( beta in alpha & x in ConwayDay beta ) ; :: thesis:
ex w being strict left-right st
( g = w & ( for x being set st x in the LeftOptions of w \/ the RightOptions of w holds
ex beta being Ordinal st
( beta in alpha & x in ConwayDay beta ) ) )

proof

reconsider w = g as strict left-right by Th4;
take w ; :: thesis:
( the LeftOptions of w = the_LeftOptions_of g & the RightOptions of w = the_RightOptions_of g ) by Def6, Def7;
hence ( g = w & ( for x being set st x in the LeftOptions of w \/ the RightOptions of w holds
ex beta being Ordinal st
( beta in alpha & x in ConwayDay beta ) ) ) by A3; :: thesis:

end;

hence g in ConwayDay alpha by Th1; :: thesis:

end;