for A being non empty Interval
for x being Real st 0 < x & A is right_open_interval holds
x ** A is right_open_interval