theorem Th125: :: FUNCT_7:126

for a, b being set holds rng (a followed_by b) = {a,b}