thus ( 1 <= i & i + 1 <= len f implies LSeg (f /. i),(f /. (i + 1)) is Subset of ) ; :: thesis: ( ( not 1 <= i or not i + 1 <= len f ) implies {} is Subset of )
assume ( i < 1 or len f < i + 1 ) ; :: thesis: {} is Subset of
{} (TOP-REAL n) is Subset of ;
hence {} is Subset of ; :: thesis: verum