theorem :: FINSEQ_3:92

for A being set st A is included_in_Seg holds
Sgm A is one-to-one ;