let x be Element of ConwayDay alpha; :: thesis: x is ConwayGame-like
take alpha ; :: according to CGAMES_1:def 3 :: thesis: x in ConwayDay alpha
thus x in ConwayDay alpha ; :: thesis: verum