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