let i be Nat; :: thesis: for f being FinSequence of the carrier of (TOP-REAL 2) st f is one-to-one & 1 <= i & i + 1 <= len f holds
not LSeg (f,i) is trivial
let f be FinSequence of the carrier of (TOP-REAL 2); :: thesis: ( f is one-to-one & 1 <= i & i + 1 <= len f implies not LSeg (f,i) is trivial )
assume A1: f is one-to-one ; :: thesis: ( not 1 <= i or not i + 1 <= len f or not LSeg (f,i) is trivial )
A2: i <> i + 1 ;
assume A3: ( 1 <= i & i + 1 <= len f ) ; :: thesis: not LSeg (f,i) is trivial
then ( i in dom f & i + 1 in dom f ) by SEQ_4:134;
then A4: f /. i <> f /. (i + 1) by A1, A2, PARTFUN2:10;
A5: ( f /. i in LSeg ((f /. i),(f /. (i + 1))) & f /. (i + 1) in LSeg ((f /. i),(f /. (i + 1))) ) by RLTOPSP1:68;
LSeg ((f /. i),(f /. (i + 1))) = LSeg (f,i) by A3, TOPREAL1:def 3;
hence not LSeg (f,i) is trivial by A4, A5, ZFMISC_1:def 10; :: thesis: verum