let i, j be Nat; :: thesis: for h being FinSequence of (TOP-REAL 2) st i in dom h & j in dom h holds
L~ (mid (h,i,j)) c= L~ h
let h be FinSequence of (TOP-REAL 2); :: thesis: ( i in dom h & j in dom h implies L~ (mid (h,i,j)) c= L~ h )
assume that
A1: i in dom h and
A2: j in dom h ; :: thesis: L~ (mid (h,i,j)) c= L~ h
A3: i <= len h by A1, FINSEQ_3:25;
A4: j <= len h by A2, FINSEQ_3:25;
A5: 1 <= j by A2, FINSEQ_3:25;
1 <= i by A1, FINSEQ_3:25;
hence L~ (mid (h,i,j)) c= L~ h by A3, A5, A4, JORDAN4:35; :: thesis: verum