let f be FinSequence of the carrier of (TOP-REAL 2); :: thesis: { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } is finite
set F = { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } ;
set F9 = { (LSeg (f,i)) where i is Nat : ( 1 <= i & i <= len f ) } ;
{ (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } c= { (LSeg (f,i)) where i is Nat : ( 1 <= i & i <= len f ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } or x in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i <= len f ) } )
assume x in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } ; :: thesis: x in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i <= len f ) }
then consider i being Nat such that
A1: ( x = LSeg (f,i) & 1 <= i ) and
A2: i + 1 <= len f ;
i <= i + 1 by NAT_1:11;
then i <= len f by A2, XXREAL_0:2;
hence x in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i <= len f ) } by A1; :: thesis: verum

end;

hence { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } is finite by Th22, FINSET_1:1; :: thesis: verum