let g be ConwayGame; :: thesis: - (- g) = g
defpred S₂[ ConwayGame] means - (- $1) <> $1;
assume not - (- g) = g ; :: thesis: contradiction
then A1: ex g being ConwayGame st S₂[g] ;
consider g being ConwayGame such that
A2: ( S₂[g] & ( for gO being ConwayGame st gO in the_Options_of g holds
not S₂[gO] ) ) from CGAMES_1:sch 2(A1);

now :: thesis: ( ( for x being object st x in the_LeftOptions_of (- (- g)) holds
x in the_LeftOptions_of g ) & ( for x being object st x in the_LeftOptions_of g holds
x in the_LeftOptions_of (- (- g)) ) )

hereby :: thesis: for x being object st x in the_LeftOptions_of g holds
x in the_LeftOptions_of (- (- g))

let x be object ; :: thesis: ( x in the_LeftOptions_of (- (- g)) implies x in the_LeftOptions_of g )
assume x in the_LeftOptions_of (- (- g)) ; :: thesis: x in the_LeftOptions_of g
then consider gR being ConwayGame such that
A3: ( gR in the_RightOptions_of (- g) & x = - gR ) by Th39;
consider gL being ConwayGame such that
A4: ( gL in the_LeftOptions_of g & gR = - gL ) by Th39, A3;
gL in the_Options_of g by A4, XBOOLE_0:def 3;
hence x in the_LeftOptions_of g by A2, A3, A4; :: thesis: verum

end;

hereby :: thesis: verum

let x be object ; :: thesis: ( x in the_LeftOptions_of g implies x in the_LeftOptions_of (- (- g)) )
assume A5: x in the_LeftOptions_of g ; :: thesis: x in the_LeftOptions_of (- (- g))
reconsider gL = x as ConwayGame by Th18, A5;
( - gL in the_RightOptions_of (- g) & gL in the_Options_of g ) by Th39, A5, XBOOLE_0:def 3;
then ( - (- gL) in the_LeftOptions_of (- (- g)) & - (- gL) = gL ) by Th39, A2;
hence x in the_LeftOptions_of (- (- g)) ; :: thesis: verum

end;

end;

then A6: the_LeftOptions_of (- (- g)) = the_LeftOptions_of g by TARSKI:2;

now :: thesis: ( ( for x being object st x in the_RightOptions_of (- (- g)) holds
x in the_RightOptions_of g ) & ( for x being object st x in the_RightOptions_of g holds
x in the_RightOptions_of (- (- g)) ) )

hereby :: thesis: for x being object st x in the_RightOptions_of g holds
x in the_RightOptions_of (- (- g))

let x be object ; :: thesis: ( x in the_RightOptions_of (- (- g)) implies x in the_RightOptions_of g )
assume x in the_RightOptions_of (- (- g)) ; :: thesis: x in the_RightOptions_of g
then consider gL being ConwayGame such that
A7: ( gL in the_LeftOptions_of (- g) & x = - gL ) by Th39;
consider gR being ConwayGame such that
A8: ( gR in the_RightOptions_of g & gL = - gR ) by Th39, A7;
gR in the_Options_of g by A8, XBOOLE_0:def 3;
hence x in the_RightOptions_of g by A2, A7, A8; :: thesis: verum

end;

hereby :: thesis: verum

let x be object ; :: thesis: ( x in the_RightOptions_of g implies x in the_RightOptions_of (- (- g)) )
assume A9: x in the_RightOptions_of g ; :: thesis: x in the_RightOptions_of (- (- g))
reconsider gR = x as ConwayGame by Th18, A9;
( - gR in the_LeftOptions_of (- g) & gR in the_Options_of g ) by Th39, A9, XBOOLE_0:def 3;
then ( - (- gR) in the_RightOptions_of (- (- g)) & - (- gR) = gR ) by Th39, A2;
hence x in the_RightOptions_of (- (- g)) ; :: thesis: verum

end;

end;

then the_RightOptions_of (- (- g)) = the_RightOptions_of g by TARSKI:2;
hence contradiction by A2, A6, Th5; :: thesis: verum