{log} ('setlog') is a satisfiability solver for formulas of the theory of\nfinite sets and finite set relation algebra (FSTRA). As such, it can be used as\nan automated theorem prover (ATP) for this theory. {log} is able to\nautomatically prove a number of FSTRA theorems, but not all of them.\nNevertheless, we have observed that many theorems that {log} cannot\nautomatically prove can be divided into a few subgoals automatically\ndischargeable by {log}. The purpose of this work is to present a prototype\ninteractive theorem prover (ITP), called {log}-ITP, providing evidence that a\nproper integration of {log} into world-class ITP's can deliver a great deal of\nproof automation concerning FSTRA. An empirical evaluation based on 210\ntheorems from the TPTP and Coq's SSReflect libraries shows a noticeable\nreduction in the size and complexity of the proofs with respect to Coq.\n