theorem :: XREAL_1:123

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