let alpha be Ordinal; :: thesis: for z being object holds
( z in ConwayDay alpha iff ex w being strict left-right st
( z = w & ( for x being set st x in the LeftOptions of w \/ the RightOptions of w holds
ex beta being Ordinal st
( beta in alpha & x in ConwayDay beta ) ) ) )
let z be object ; :: thesis: ( z in ConwayDay alpha iff ex w being strict left-right st
( z = w & ( for x being set st x in the LeftOptions of w \/ the RightOptions of w holds
ex beta being Ordinal st
( beta in alpha & x in ConwayDay beta ) ) ) )
consider f being Sequence such that
A1: ( alpha in dom f & f . alpha = ConwayDay alpha & S₁[f] ) by Def2;

hereby :: thesis: ( ex w being strict left-right st
( z = w & ( for x being set st x in the LeftOptions of w \/ the RightOptions of w holds
ex beta being Ordinal st
( beta in alpha & x in ConwayDay beta ) ) ) implies z in ConwayDay alpha )

assume z in ConwayDay alpha ; :: thesis: ex w being strict left-right st
( 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 alpha & e in ConwayDay beta ) ) )
then z in H₁(f | alpha) by A1;
then consider x, y being Subset of (union (rng (f | alpha))) such that
A2: z = left-right(# x,y #) ;
reconsider w = z as strict left-right by A2;
take w = w; :: thesis: ( 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 alpha & e in ConwayDay beta ) ) )
thus z = w ; :: thesis: for e being set st e in the LeftOptions of w \/ the RightOptions of w holds
ex beta being Ordinal st
( beta in alpha & e in ConwayDay beta )
let e be set ; :: thesis: ( e in the LeftOptions of w \/ the RightOptions of w implies ex beta being Ordinal st
( beta in alpha & e in ConwayDay beta ) )
assume e in the LeftOptions of w \/ the RightOptions of w ; :: thesis: ex beta being Ordinal st
( beta in alpha & e in ConwayDay beta )
then ( e in x or e in y ) by A2, XBOOLE_0:def 3;
then consider r being set such that
A3: ( e in r & r in rng (f | alpha) ) by TARSKI:def 4;
ex beta being object st
( beta in dom (f | alpha) & r = (f | alpha) . beta ) by A3, FUNCT_1:def 3;
then consider beta being Ordinal such that
A4: ( beta in dom (f | alpha) & r = (f | alpha) . beta ) ;
take beta = beta; :: thesis: ( beta in alpha & e in ConwayDay beta )
dom (f | alpha) c= alpha by RELAT_1:58;
hence beta in alpha by A4; :: thesis: e in ConwayDay beta
dom (f | alpha) c= dom f by RELAT_1:60;
then f . beta = ConwayDay beta by A1, Def2, A4;
hence e in ConwayDay beta by A3, A4, FUNCT_1:47; :: thesis: verum

end;

hereby :: thesis: verum

assume ex w being strict left-right st
( z = w & ( for x being set st x in the LeftOptions of w \/ the RightOptions of w holds
ex beta being Ordinal st
( beta in alpha & x in ConwayDay beta ) ) ) ; :: thesis: z in ConwayDay alpha
then consider w being strict left-right such that
A5: ( w = z & ( for x being set st x in the LeftOptions of w \/ the RightOptions of w holds
ex beta being Ordinal st
( beta in alpha & x in ConwayDay beta ) ) ) ;
( the LeftOptions of w is Subset of (union (rng (f | alpha))) & the RightOptions of w is Subset of (union (rng (f | alpha))) )

proof

the LeftOptions of w \/ the RightOptions of w c= union (rng (f | alpha))

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in the LeftOptions of w \/ the RightOptions of w or e in union (rng (f | alpha)) )
assume e in the LeftOptions of w \/ the RightOptions of w ; :: thesis: e in union (rng (f | alpha))
then consider beta being Ordinal such that
A6: ( beta in alpha & e in ConwayDay beta ) by A5;
A7: alpha c= dom f by A1, ORDINAL1:def 2;
then f . beta = ConwayDay beta by Def2, A1, A6;
then ConwayDay beta c= union (rng (f | alpha)) by A6, A7, FUNCT_1:50, ZFMISC_1:74;
hence e in union (rng (f | alpha)) by A6; :: thesis: verum

end;

hence ( the LeftOptions of w is Subset of (union (rng (f | alpha))) & the RightOptions of w is Subset of (union (rng (f | alpha))) ) by XBOOLE_1:11; :: thesis: verum

end;

then w in H₁(f | alpha) ;
hence z in ConwayDay alpha by A1, A5; :: thesis: verum

end;