let g be ConwayGame; :: thesis: ( g = ConwayZero iff the_Options_of g = {} )

hereby :: thesis: ( the_Options_of g = {} implies g = ConwayZero )

assume g = ConwayZero ; :: thesis: the_Options_of g = {}
then ( the_LeftOptions_of g = {} & the_RightOptions_of g = {} ) ;
hence the_Options_of g = {} ; :: thesis: verum

end;

hereby :: thesis: verum

reconsider w = g as strict left-right by Th4;
assume the_Options_of g = {} ; :: thesis: g = ConwayZero
then ( the_LeftOptions_of g = {} & the_RightOptions_of g = {} ) ;
then ( the LeftOptions of w = {} & the RightOptions of w = {} ) by Def6, Def7;
hence g = ConwayZero ; :: thesis: verum

end;