let f be FinSequence of (TOP-REAL 2); :: thesis: for i being Element of NAT st 1 <= i & i + 1 <= len f holds
LSeg (f /. i),(f /. (i + 1)) c= L~ f
let i be Element of NAT ; :: thesis: ( 1 <= i & i + 1 <= len f implies LSeg (f /. i),(f /. (i + 1)) c= L~ f )
assume that
A1: 1 <= i and
A2: i + 1 <= len f ; :: thesis: LSeg (f /. i),(f /. (i + 1)) c= L~ f
LSeg f,i = LSeg (f /. i),(f /. (i + 1)) by A1, A2, TOPREAL1:def 5;
hence LSeg (f /. i),(f /. (i + 1)) c= L~ f by TOPREAL3:26; :: thesis: verum