assume - x >= 0 ; :: according to XXREAL_0:def 7 :: thesis: contradiction
then (- x) - (- x) > 0 ;
hence contradiction by Th7; :: thesis: verum