for X being non empty set
for s, s1 being sequence of X st s is V30() & s1 is subsequence of s holds
s = s1