:: deftheorem defines ProductLeftOpenIntervals SRINGS_5:def 9 :
for n being non zero Nat holds ProductLeftOpenIntervals n = (Seg n) --> the_set_of_all_left_open_real_bounded_intervals;