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