:: deftheorem defines special TOPREAL1:def 5 :
for IT being FinSequence of (TOP-REAL 2) holds
( IT is special iff for i being Nat st 1 <= i & i + 1 <= len IT & not (IT /. i) `1 = (IT /. (i + 1)) `1 holds
(IT /. i) `2 = (IT /. (i + 1)) `2 );