theorem Th25: :: TOPREAL8:25
for m, n being Nat
for f being non empty special FinSequence of (TOP-REAL 2) holds (m,n) -cut f is special