for g, gO being ConwayGame holds
( ( gO in the_LeftOptions_of (- g) implies - gO in the_RightOptions_of g ) & ( - gO in the_RightOptions_of g implies gO in the_LeftOptions_of (- g) ) & ( gO in the_LeftOptions_of g implies - gO in the_RightOptions_of (- g) ) & ( - gO in the_RightOptions_of (- g) implies gO in the_LeftOptions_of g ) & ( gO in the_RightOptions_of (- g) implies - gO in the_LeftOptions_of g ) & ( - gO in the_LeftOptions_of g implies gO in the_RightOptions_of (- g) ) & ( gO in the_RightOptions_of g implies - gO in the_LeftOptions_of (- g) ) & ( - gO in the_LeftOptions_of (- g) implies gO in the_RightOptions_of g ) )