Cyclic and, more generally, non-well-founded proofs turn out to be an interesting alternative to traditional proofs for logics with fixed-point operators. Proof systems allowing such kind of proofs can be defined for the modal mu-calculus, the Lambek calculus with iteration, Peano arithmetic, and for other systems. In this talk, we consider a sequent calculus allowing non-well-founded proofs for the modal logic of transitive closure K+ and discuss a syntactic cut-elimination theorem for the given system.