reconsider VAR9 = VAR as non empty Subset of NAT ;
reconsider x9 = x as Element of VAR9 ;
reconsider x9 = x9 as Element of NAT ;
<*x9*> is FinSequence of NAT ;
hence <*x*> is FinSequence of NAT ; :: thesis: verum