set F = { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } ;
{ (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } c= bool the carrier of (TOP-REAL n)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } or a in bool the carrier of (TOP-REAL n) )
assume a in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } ; :: thesis: a in bool the carrier of (TOP-REAL n)
then ex i being Nat st
( a = LSeg (f,i) & 1 <= i & i + 1 <= len f ) ;
hence a in bool the carrier of (TOP-REAL n) ; :: thesis: verum

end;

then reconsider F = { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } as Subset-Family of (TOP-REAL n) ;
union F is Subset of (TOP-REAL n) ;
hence union { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } is Subset of (TOP-REAL n) ; :: thesis: verum