let n be Element of 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 set ; :: 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
A2: i in NAT by ORDINAL1:def 12;

now

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

case i < 1 ; :: thesis: contradiction

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

end;

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

now

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 A4: i + 1 <= len f ; :: thesis: x in L~ f

set M = { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ;
LSeg (f,i) in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A2, A3, A4;
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