let alpha be Ordinal; :: thesis: for g being ConwayGame holds
( g in ConwayDay alpha iff for x being set st x in the_Options_of g holds
ex beta being Ordinal st
( beta in alpha & x in ConwayDay beta ) )
let g be ConwayGame; :: thesis: ( g in ConwayDay alpha iff for x being set st x in the_Options_of g holds
ex beta being Ordinal st
( beta in alpha & x in ConwayDay beta ) )

hereby :: thesis: ( ( for x being set st x in the_Options_of g holds
ex beta being Ordinal st
( beta in alpha & x in ConwayDay beta ) ) implies g in ConwayDay alpha )

assume g in ConwayDay alpha ; :: thesis: for x being set st x in the_Options_of g holds
ex beta being Ordinal st
( beta in alpha & x in ConwayDay beta )
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: ( x in the_Options_of g implies ex beta being Ordinal st
( beta in alpha & x in ConwayDay beta ) )
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: ex beta being Ordinal st
( beta in alpha & x in ConwayDay beta )
hence ex beta being Ordinal st
( beta in alpha & x in ConwayDay beta ) by A1, A2; :: thesis: verum

end;

hereby :: thesis: verum

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: g in ConwayDay alpha
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: ( 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 ) ) )
( 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: verum

end;

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

end;