let w be strict left-right ; :: thesis:

hereby :: thesis:

assume w is ConwayGame ; :: thesis:
then reconsider g = w as ConwayGame ;
( the LeftOptions of w = the_LeftOptions_of g & the RightOptions of w = the_RightOptions_of g ) by Def6, Def7;
then the LeftOptions of w \/ the RightOptions of w = the_Options_of g ;
hence for z being set st z in the LeftOptions of w \/ the RightOptions of w holds
z is ConwayGame by Th17; :: thesis:

end;

hereby :: thesis:

assume A1: for z being set st z in the LeftOptions of w \/ the RightOptions of w holds
z is ConwayGame ; :: thesis:
set Z = { (ConwayRank z) where z is Element of the LeftOptions of w \/ the RightOptions of w : verum } ;
set alpha = sup { (ConwayRank z) where z is Element of the LeftOptions of w \/ the RightOptions of w : verum } ;

now :: thesis:

let z be set ; :: thesis:
assume A2: z in the LeftOptions of w \/ the RightOptions of w ; :: thesis:
then ConwayRank z in { (ConwayRank z) where z is Element of the LeftOptions of w \/ the RightOptions of w : verum } ;
then ( ConwayRank z in On { (ConwayRank z) where z is Element of the LeftOptions of w \/ the RightOptions of w : verum } & On { (ConwayRank z) where z is Element of the LeftOptions of w \/ the RightOptions of w : verum } c= sup { (ConwayRank z) where z is Element of the LeftOptions of w \/ the RightOptions of w : verum } ) by ORDINAL1:def 9, ORDINAL2:def 3;
then A3: ConwayRank z c= sup { (ConwayRank z) where z is Element of the LeftOptions of w \/ the RightOptions of w : verum } by ORDINAL1:def 2;
take beta = sup { (ConwayRank z) where z is Element of the LeftOptions of w \/ the RightOptions of w : verum } ; :: thesis:
thus beta in succ (sup { (ConwayRank z) where z is Element of the LeftOptions of w \/ the RightOptions of w : verum } ) by ORDINAL1:6; :: thesis:
z is ConwayGame by A1, A2;
hence z in ConwayDay beta by A3, Th12; :: thesis:

end;

then w in ConwayDay (succ (sup { (ConwayRank z) where z is Element of the LeftOptions of w \/ the RightOptions of w : verum } )) by Th1;
hence w is ConwayGame ; :: thesis:

end;