:: deftheorem defines being_S-Seq TOPREAL1:def 8 :
for f being FinSequence of (TOP-REAL 2) holds
( f is being_S-Seq iff ( f is one-to-one & len f >= 2 & f is unfolded & f is s.n.c. & f is special ) );