for f being FinSequence of the carrier of (TOP-REAL 2) holds { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } is finite