theorem Th7: :: RCOMP_1:7

for p, q being Real holds ].p,q.[ is open