theorem Th1: :: FSCIRC_1:1

for x, y, c being set holds InnerVertices (BorrowStr (x,y,c)) is Relation