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