let x be Surreal; :: thesis: ( L_ (- x) = -- (R_ x) & R_ (- x) = -- (L_ x) )
- x = [(-- (R_ x)),(-- (L_ x))] by Th7;
hence ( L_ (- x) = -- (R_ x) & R_ (- x) = -- (L_ x) ) ; :: thesis: verum