let g, gO be ConwayGame; :: thesis: ( ( 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 ) )
( g = - (- g) & gO = - (- gO) ) by Th40;
hence ( ( 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 ) ) by Th39; :: thesis: verum