let i, j be Element of 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 ( i in dom h & j in dom h ) ; :: thesis: L~ (mid h,i,j) c= L~ h
then ( 1 <= i & i <= len h & 1 <= j & j <= len h ) by FINSEQ_3:27;
hence L~ (mid h,i,j) c= L~ h by JORDAN4:47; :: thesis: verum