let n be non zero Nat; for x being Element of Product (n,the_set_of_all_left_open_real_bounded_intervals) ex 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).] )
let x be Element of Product (n,the_set_of_all_left_open_real_bounded_intervals); ex 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).] )
consider s being Tuple of n, the_set_of_all_left_open_real_bounded_intervals such that
A1:
for t being Element of REAL n holds
( ( for i being Nat st i in Seg n holds
t . i in s . i ) iff t in x )
by Th42;
consider a, b being Element of REAL n such that
A2:
for i being Nat st i in Seg n holds
s . i = ].(a . i),(b . i).]
by Th54;
take
a
; ex 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).] )
take
b
; 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).] )
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).] )
hence
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).] )
; verum