:: deftheorem defines L~ TOPREAL1:def 4 :
for n being Nat
for f being FinSequence of (TOP-REAL n) holds L~ f = union { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } ;