theorem :: XREAL_1:58

for a being Real holds
( a < 0 iff 0 < - a ) ;