let n be Nat; :: thesis: for f being FinSequence of (TOP-REAL n)
for i being Nat holds LSeg (f,i) c= L~ f
let f be FinSequence of (TOP-REAL n); :: thesis: for i being Nat holds LSeg (f,i) c= L~ f
let i be Nat; :: thesis: LSeg (f,i) c= L~ f
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in LSeg (f,i) or x in L~ f )
assume A1: x in LSeg (f,i) ; :: thesis: x in L~ f

now :: thesis: ( ( i < 1 & contradiction ) or ( i >= 1 & x in L~ f ) )

per cases ( i < 1 or i >= 1 ) ;

case i < 1 ; :: thesis: contradiction

hence contradiction by A1, TOPREAL1:def 3; :: thesis: verum

end;

case A2: i >= 1 ; :: thesis: x in L~ f

now :: thesis: ( ( i + 1 > len f & contradiction ) or ( i + 1 <= len f & x in L~ f ) )

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

case i + 1 > len f ; :: thesis: contradiction

hence contradiction by A1, TOPREAL1:def 3; :: thesis: verum

end;

case A3: i + 1 <= len f ; :: thesis: x in L~ f

set M = { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } ;
LSeg (f,i) in { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } by A2, A3;
hence x in L~ f by A1, TARSKI:def 4; :: thesis: verum

end;

end;

end;

hence x in L~ f ; :: thesis: verum

end;

end;

end;

hence x in L~ f ; :: thesis: verum