theorem Th13: :: RFINSEQ:13

for r being Real holds MIM <*r*> = <*r*>