let Q be Subset of (TOP-REAL 2); :: thesis: for f being FinSequence of the carrier of (TOP-REAL 2) st Q = union { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } holds
Q is closed
let f be FinSequence of the carrier of (TOP-REAL 2); :: thesis: ( Q = union { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } implies Q is closed )
reconsider F = { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } as Subset-Family of (TOP-REAL 2) by Th25;

now :: thesis: for P being Subset of (TOP-REAL 2) st P in F holds
P is closed

let P be Subset of (TOP-REAL 2); :: thesis: ( P in F implies P is closed )
assume P in F ; :: thesis: P is closed
then ex i being Nat st
( LSeg (f,i) = P & 1 <= i & i + 1 <= len f ) ;
hence P is closed ; :: thesis: verum

end;

then A1: F is closed by TOPS_2:def 2;
F is finite by Th23;
hence ( Q = union { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } implies Q is closed ) by A1, TOPS_2:21; :: thesis: verum