theorem Th12: :: FSCIRC_2:12

for x, y, c being set holds InnerVertices (BorrowIStr (x,y,c)) = {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]}