let alpha be Ordinal; :: thesis:
let z be object ; :: thesis:
consider f being Sequence such that
A1: ( alpha in dom f & f . alpha = ConwayDay alpha & S₁[f] ) by Def2;

assume z in ConwayDay alpha ; :: thesis:
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:
thus z = w ; :: thesis:
let e be set ; :: thesis:
assume e in the LeftOptions of w \/ the RightOptions of w ; :: thesis:
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:
dom (f | alpha) c= alpha by RELAT_1:58;
hence beta in alpha by A4; :: thesis:
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:

end;

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

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume e in the LeftOptions of w \/ the RightOptions of w ; :: thesis:
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:

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:

end;

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

end;