theorem Th2: :: POLYVIE1:2

for X being finite set holds canFS X is Enumeration of X