theorem Th19: :: TOPREAL8:19
for f being non trivial FinSequence of (TOP-REAL 2) holds LSeg (f,1) = L~ (f | 2)