theorem Th5: :: FOMODEL0:5

for D being non empty set
for x being set holds
( x is non empty FinSequence of D iff x in (D *) \ {{}} )