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