let x be Surreal; :: thesis: born_eq x = born_eq (- x)
consider y being Surreal such that
A1: ( born y = born_eq x & y == x ) by SURREALO:def 5;
A2: - y == - x by A1, Th10;
A3: born y = born (- y) by Th12;
for z being Surreal st z == - x holds
born y c= born z

proof

let z be Surreal; :: thesis: ( z == - x implies born y c= born z )
assume z == - x ; :: thesis: born y c= born z
then ( - z == - (- x) & - (- x) = x ) by Th10;
then born_eq x c= born (- z) by SURREALO:def 5;
hence born y c= born z by A1, Th12; :: thesis: verum

end;

hence born_eq x = born_eq (- x) by A1, A2, A3, SURREALO:def 5; :: thesis: verum