theorem Th7: :: FSCIRC_1:7

for x, y, c being set holds
( [<*x,y*>,and2a] in InnerVertices (BorrowStr (x,y,c)) & [<*y,c*>,and2] in InnerVertices (BorrowStr (x,y,c)) & [<*x,c*>,and2a] in InnerVertices (BorrowStr (x,y,c)) )