theorem ThCanFSIsMss: :: GROUP_23:2

for A being finite set holds canFS A is ManySortedSet of Seg (card A)