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