:: deftheorem defines unfolded TOPREAL1:def 6 :
for IT being FinSequence of (TOP-REAL 2) holds
( IT is unfolded iff for i being Nat st 1 <= i & i + 2 <= len IT holds
(LSeg (IT,i)) /\ (LSeg (IT,(i + 1))) = {(IT /. (i + 1))} );