theorem :: SPPOL_1:24

for f being FinSequence of the carrier of (TOP-REAL 2) holds { (LSeg (f,i)) where i is Nat : ( 1 <= i & i <= len f ) } is Subset-Family of (TOP-REAL 2)