let x, y, c be set ; ( [<*x,y*>,and2a] in InnerVertices (BorrowStr (x,y,c)) & [<*y,c*>,and2] in InnerVertices (BorrowStr (x,y,c)) & [<*x,c*>,and2a] in InnerVertices (BorrowStr (x,y,c)) )
[<*x,y*>,and2a] in InnerVertices (1GateCircStr (<*x,y*>,and2a))
by FACIRC_1:47;
then
[<*x,y*>,and2a] in InnerVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)))
by FACIRC_1:21;
then A1:
[<*x,y*>,and2a] in InnerVertices (BorrowIStr (x,y,c))
by FACIRC_1:21;
[<*y,c*>,and2] in InnerVertices (1GateCircStr (<*y,c*>,and2))
by FACIRC_1:47;
then
[<*y,c*>,and2] in InnerVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)))
by FACIRC_1:21;
then A2:
[<*y,c*>,and2] in InnerVertices (BorrowIStr (x,y,c))
by FACIRC_1:21;
[<*x,c*>,and2a] in InnerVertices (1GateCircStr (<*x,c*>,and2a))
by FACIRC_1:47;
then
[<*x,c*>,and2a] in InnerVertices (BorrowIStr (x,y,c))
by FACIRC_1:21;
hence
( [<*x,y*>,and2a] in InnerVertices (BorrowStr (x,y,c)) & [<*y,c*>,and2] in InnerVertices (BorrowStr (x,y,c)) & [<*x,c*>,and2a] in InnerVertices (BorrowStr (x,y,c)) )
by A1, A2, FACIRC_1:21; verum