for f being FinSequence of (TOP-REAL 2) st f is special & 2 <= len f & f . 1 <> f . (len f) holds
ex g being FinSequence of (TOP-REAL 2) st
( 2 <= len g & g is special & g is one-to-one & L~ g c= L~ f & f . 1 = g . 1 & f . (len f) = g . (len g) & rng g c= rng f )