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