let i be Element of 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 )
assume A2: ( 1 <= i & i + 1 <= len f ) ; :: thesis: not LSeg f,i is trivial
then A3: ( i in dom f & i + 1 in dom f ) by GOBOARD2:3;
i <> i + 1 ;
then A4: f /. i <> f /. (i + 1) by A1, A3, PARTFUN2:17;
A5: ( f /. i in LSeg (f /. i),(f /. (i + 1)) & f /. (i + 1) in LSeg (f /. i),(f /. (i + 1)) ) by RLTOPSP1:69;
LSeg (f /. i),(f /. (i + 1)) = LSeg f,i by A2, TOPREAL1:def 5;
hence not LSeg f,i is trivial by A4, A5, REALSET1:15; :: thesis: verum