let g be ConwayGame; :: thesis: not g in the_Options_of g
assume g in the_Options_of g ; :: thesis: contradiction
then ConwayRank g in ConwayRank g by Th14;
hence contradiction ; :: thesis: verum