theorem Th6: :: FSCIRC_1:6

for x, y, c being set holds
( x in the carrier of (BorrowStr (x,y,c)) & y in the carrier of (BorrowStr (x,y,c)) & c in the carrier of (BorrowStr (x,y,c)) )