theorem Th45: :: SRINGS_5:62

for n being non zero Nat
for x being Subset of (REAL n)
for a, b being Element of REAL n st ( for t being Element of REAL n holds
( t in x iff for i being Nat st i in Seg n holds
t . i in [.(a . i),(b . i).[ ) ) holds
x is Element of Product (n,the_set_of_all_right_open_real_bounded_intervals)