(a,b) followed_by c = (a followed_by c) +* (1,b) by Th124;
hence (a,b) followed_by c is sequence of X by Th114; :: thesis: verum