theorem Th7: :: URYSOHN2:7

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