theorem :: FINSEQ_2:90

for D being set
for D9 being FinSequenceSet of D holds D9 c= D *