for n being non zero Nat holds ProductLeftOpenIntervals n = (Seg n) --> { ].a,b.] where a, b is Real : verum } ;