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