theorem Th37: :: FINSEQ_3:39

for A being included_in_Seg set holds len (Sgm A) = card A