let w be strict left-right ; :: thesis: ( w is ConwayGame iff for z being set st z in the LeftOptions of w \/ the RightOptions of w holds
z is ConwayGame )

hereby :: thesis: ( ( for z being set st z in the LeftOptions of w \/ the RightOptions of w holds
z is ConwayGame ) implies w is ConwayGame )

assume w is ConwayGame ; :: thesis: for z being set st z in the LeftOptions of w \/ the RightOptions of w holds
z is ConwayGame
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: verum

end;

hereby :: thesis: verum

assume A1: for z being set st z in the LeftOptions of w \/ the RightOptions of w holds
z is ConwayGame ; :: thesis: w is ConwayGame
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: for z being set st z in the LeftOptions of w \/ the RightOptions of w holds
ex beta being set st
( beta in succ (sup { (ConwayRank z) where z is Element of the LeftOptions of w \/ the RightOptions of w : verum } ) & z in ConwayDay beta )

let z be set ; :: thesis: ( z in the LeftOptions of w \/ the RightOptions of w implies ex beta being set st
( beta in succ (sup { (ConwayRank z) where z is Element of the LeftOptions of w \/ the RightOptions of w : verum } ) & z in ConwayDay beta ) )
assume A2: z in the LeftOptions of w \/ the RightOptions of w ; :: thesis: ex beta being set st
( beta in succ (sup { (ConwayRank z) where z is Element of the LeftOptions of w \/ the RightOptions of w : verum } ) & z in ConwayDay beta )
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: ( beta in succ (sup { (ConwayRank z) where z is Element of the LeftOptions of w \/ the RightOptions of w : verum } ) & z in ConwayDay beta )
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 in ConwayDay beta
z is ConwayGame by A1, A2;
hence z in ConwayDay beta by A3, Th12; :: thesis: verum

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: verum

end;