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