let g be ConwayGame; :: thesis: g is strict left-right
consider alpha being Ordinal such that
A1: g in ConwayDay alpha by Def3;
ex w being strict left-right st
( w = g & ( 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 ) ) ) by A1, Th1;
hence g is strict left-right ; :: thesis: verum