A1: ConwayDay 0 c= {ConwayZero}

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in ConwayDay 0 ; :: thesis:
then consider w being strict left-right such that
A2: ( z = w & ( for e being set st e in the LeftOptions of w \/ the RightOptions of w holds
ex beta being Ordinal st
( beta in 0 & e in ConwayDay beta ) ) ) by Th1;
the LeftOptions of w \/ the RightOptions of w = {}

assume not the LeftOptions of w \/ the RightOptions of w = {} ; :: thesis:
then consider e being object such that
A3: e in the LeftOptions of w \/ the RightOptions of w by XBOOLE_0:def 1;
ex beta being Ordinal st
( beta in 0 & e in ConwayDay beta ) by A2, A3;
hence contradiction ; :: thesis:

end;

then ( the LeftOptions of w = {} & the RightOptions of w = {} ) ;
hence z in {ConwayZero} by A2, TARSKI:def 1; :: thesis:

end;

for e being set st e in {} \/ {} holds
ex beta being Ordinal st
( beta in 0 & e in ConwayDay beta ) ;
then ConwayZero in ConwayDay 0 by Th1;
then {ConwayZero} c= ConwayDay 0 by ZFMISC_1:31;
hence ConwayDay 0 = {ConwayZero} by A1, XBOOLE_0:def 10; :: thesis: