theorem Th25: :: TOPREAL1:25

for h being FinSequence of (TOP-REAL 2) st h is being_S-Seq holds
L~ h is_an_arc_of h /. 1,h /. (len h)