theorem Th5: :: FINSEQ_1:5

for a, b being natural Number holds
( a <= b iff Seg a c= Seg b )