theorem :: VALUED_0:19

for XX being non empty set
for ss being sequence of XX holds ss is subsequence of ss