for a, b being Real st a " < 0 & 0 < b " holds
a < b