:: deftheorem defines s.n.c. TOPREAL1:def 7 :
for IT being FinSequence of (TOP-REAL 2) holds
( IT is s.n.c. iff for i, j being Nat st i + 1 < j holds
LSeg (IT,i) misses LSeg (IT,j) );