theorem Th14: :: JORDAN2B:14

for n being Element of NAT
for P being Subset of (TOP-REAL n)
for a, b being Real
for i being Element of NAT st P = { p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b ) } & i in Seg n holds
P is open