for a, b being set holds (a followed_by b) . 0 = a