thus (a,b) followed_by c is SetSequence of Omega ; :: thesis: verum