theorem Th2: :: FSCIRC_1:2

for x, y, c being non pair set holds InputVertices (BorrowStr (x,y,c)) is without_pairs