:: deftheorem defines BorrowICirc FSCIRC_1:def 5 :
for x, y, c being set holds BorrowICirc (x,y,c) = ((1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2))) +* (1GateCircuit (x,c,and2a));