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 ( 1 <= i & i + 1 <= len f ) ; :: thesis: LSeg (f /. i),(f /. (i + 1)) c= L~ f
then LSeg f,i = LSeg (f /. i),(f /. (i + 1)) by TOPREAL1:def 5;
hence LSeg (f /. i),(f /. (i + 1)) c= L~ f by TOPREAL3:26; :: thesis: verum