let g1, g2 be ConwayGame; :: thesis: ( g1 = g2 iff ( the_LeftOptions_of g1 = the_LeftOptions_of g2 & the_RightOptions_of g1 = the_RightOptions_of g2 ) )
thus ( g1 = g2 implies ( the_LeftOptions_of g1 = the_LeftOptions_of g2 & the_RightOptions_of g1 = the_RightOptions_of g2 ) ) ; :: thesis: ( the_LeftOptions_of g1 = the_LeftOptions_of g2 & the_RightOptions_of g1 = the_RightOptions_of g2 implies g1 = g2 )
reconsider w1 = g1 as strict left-right by Th4;
reconsider w2 = g2 as strict left-right by Th4;
assume A1: ( the_LeftOptions_of g1 = the_LeftOptions_of g2 & the_RightOptions_of g1 = the_RightOptions_of g2 ) ; :: thesis: g1 = g2
( the LeftOptions of w1 = the_LeftOptions_of g1 & the LeftOptions of w2 = the_LeftOptions_of g2 & the RightOptions of w1 = the_RightOptions_of g1 & the RightOptions of w2 = the_RightOptions_of g2 ) by Def6, Def7;
hence g1 = g2 by A1; :: thesis: verum