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 )

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

end;

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