let x, y, c be set ; :: thesis: ( [<*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; :: thesis: verum