for alpha being Ordinal
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 ) ) ) )