for a, b being set holds dom (a followed_by b) = NAT