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