theorem Th8: :: FSCIRC_1:8

for x, y, c being non pair set holds
( x in InputVertices (BorrowStr (x,y,c)) & y in InputVertices (BorrowStr (x,y,c)) & c in InputVertices (BorrowStr (x,y,c)) )