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

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 & i <> k & i <> k + 1 ) ;
hence P is closed ; :: thesis: verum

end;

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