set w = left-right(# {ConwayZero},{} #);
for x being set st x in the LeftOptions of left-right(# {ConwayZero},{} #) \/ the RightOptions of left-right(# {ConwayZero},{} #) holds
ex beta being Ordinal st
( beta in 1 & x in ConwayDay beta )

proof

let x be set ; :: thesis: ( x in the LeftOptions of left-right(# {ConwayZero},{} #) \/ the RightOptions of left-right(# {ConwayZero},{} #) implies ex beta being Ordinal st
( beta in 1 & x in ConwayDay beta ) )
assume x in the LeftOptions of left-right(# {ConwayZero},{} #) \/ the RightOptions of left-right(# {ConwayZero},{} #) ; :: thesis: ex beta being Ordinal st
( beta in 1 & x in ConwayDay beta )
then A1: x = ConwayZero by TARSKI:def 1;
take 0 ; :: thesis: ( 0 in 1 & x in ConwayDay 0 )
1 = succ 0 ;
hence ( 0 in 1 & x in ConwayDay 0 ) by A1, ORDINAL1:6; :: thesis: verum

end;

hence left-right(# {ConwayZero},{} #) is Element of ConwayDay 1 by Th1; :: thesis: verum