consider r being Real such that
A1: x == uReal . r by Th62;
( - x == - (uReal . r) & - (uReal . r) == uReal . (- r) ) by A1, Th56, SURREALR:65;
then - x == uReal . (- r) by SURREALO:4;
hence - x is *real by Th62; :: thesis: verum