A1: ConwayDay 0 c= {ConwayZero}

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in ConwayDay 0 or z in {ConwayZero} )
assume z in ConwayDay 0 ; :: thesis: z in {ConwayZero}
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 = {}

proof

assume not the LeftOptions of w \/ the RightOptions of w = {} ; :: thesis: contradiction
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: verum

end;

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

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