theorem Th7: :: CALCUL_2:7

for a, b being Nat holds seq (a,b) c= Seg (a + b)