theorem Th11: :: URYSOHN2:11

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