let g, gO be ConwayGame; :: thesis: ( ( gO in the_LeftOptions_of g or gO in the_RightOptions_of g ) implies ConwayRank gO in ConwayRank g )
assume ( gO in the_LeftOptions_of g or gO in the_RightOptions_of g ) ; :: thesis: ConwayRank gO in ConwayRank g
then gO in the_Options_of g by XBOOLE_0:def 3;
hence ConwayRank gO in ConwayRank g by Th14; :: thesis: verum