for i, j, n being Nat st i < j & j in Segm n holds
i in Segm n