theorem Th54: :: SRINGS_5:83

for n being non zero Nat
for s being Tuple of n, the_set_of_all_left_open_real_bounded_intervals ex a, b being Element of REAL n st
for i being Nat st i in Seg n holds
s . i = ].(a . i),(b . i).]