let x, y, c be set ; :: thesis: ( 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) )
y in the carrier of (1GateCircStr <*x,y*>,and2a ) by FACIRC_1:43;
then A1: y in the carrier of ((1GateCircStr <*x,y*>,and2a ) +* (1GateCircStr <*y,c*>,and2 )) by FACIRC_1:20;
( x in the carrier of (1GateCircStr <*x,c*>,and2a ) & c in the carrier of (1GateCircStr <*x,c*>,and2a ) ) by FACIRC_1:43;
then ( x in the carrier of (BorrowIStr x,y,c) & y in the carrier of (BorrowIStr x,y,c) & c in the carrier of (BorrowIStr x,y,c) ) by A1, FACIRC_1:20;
hence ( 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) ) by FACIRC_1:20; :: thesis: verum