:: deftheorem defines BorrowIStr FSCIRC_1:def 3 :
for x, y, c being set holds BorrowIStr (x,y,c) = ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a));