take <*ConwayZero*> ; :: thesis: ( <*ConwayZero*> is ConwayGame-valued & not <*ConwayZero*> is empty )
thus ( <*ConwayZero*> is ConwayGame-valued & not <*ConwayZero*> is empty ) ; :: thesis: verum