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