let n be Nat; :: thesis: for f being FinSequence of () st 2 <= len f holds
( f . 1 in L~ f & f /. 1 in L~ f & f . (len f) in L~ f & f /. (len f) in L~ f )

let f be FinSequence of (); :: thesis: ( 2 <= len f implies ( f . 1 in L~ f & f /. 1 in L~ f & f . (len f) in L~ f & f /. (len f) in L~ f ) )
assume A1: 2 <= len f ; :: thesis: ( f . 1 in L~ f & f /. 1 in L~ f & f . (len f) in L~ f & f /. (len f) in L~ f )
then A2: 1 + 1 <= len f ;
then A3: LSeg (f,1) in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } ;
f /. 1 in LSeg ((f /. 1),(f /. (1 + 1))) by RLTOPSP1:68;
then f /. 1 in LSeg (f,1) by ;
then f /. 1 in union { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } by ;
then A4: f /. 1 in L~ f by TOPREAL1:def 4;
A5: ((len f) -' 1) + 1 = len f by ;
A6: 1 <= (len f) -' 1 by ;
then A7: LSeg (f,((len f) -' 1)) in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } by A5;
f /. (len f) in LSeg ((f /. ((len f) -' 1)),(f /. (((len f) -' 1) + 1))) by ;
then f /. (len f) in LSeg (f,((len f) -' 1)) by ;
then f /. (len f) in union { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } by ;
then A8: f /. (len f) in L~ f by TOPREAL1:def 4;
1 <= len f by ;
hence ( f . 1 in L~ f & f /. 1 in L~ f & f . (len f) in L~ f & f /. (len f) in L~ f ) by ; :: thesis: verum