per cases ( ( 1 <= i & i + 1 <= len f ) or not 1 <= i or not i + 1 <= len f ) ;

suppose ( 1 <= i & i + 1 <= len f ) ; :: thesis: LSeg (f,i) is closed

then LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by TOPREAL1:def 3;
hence LSeg (f,i) is closed ; :: thesis: verum

end;

suppose A1: ( not 1 <= i or not i + 1 <= len f ) ; :: thesis: LSeg (f,i) is closed

{} (TOP-REAL 2) is closed ;
hence LSeg (f,i) is closed by A1, TOPREAL1:def 3; :: thesis: verum

end;

end;