let x, y, c be non pair set ; :: thesis: not InputVertices (BorrowStr x,y,c) is with_pair
set M = BorrowStr x,y,c;
set MI = BorrowIStr x,y,c;
set S = 1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 ;
A1: ( not InputVertices (1GateCircStr <*x,y*>,and2a ) is with_pair & not InputVertices (1GateCircStr <*x,c*>,and2a ) is with_pair & not InputVertices (1GateCircStr <*y,c*>,and2 ) is with_pair ) by FACIRC_1:41;
then not InputVertices ((1GateCircStr <*x,y*>,and2a ) +* (1GateCircStr <*y,c*>,and2 )) is with_pair by FACIRC_1:9;
then A2: not InputVertices (BorrowIStr x,y,c) is with_pair by A1, FACIRC_1:9;
InnerVertices (1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 ) is Relation by FACIRC_1:38;
then A3: InputVertices (BorrowStr x,y,c) = (InputVertices (BorrowIStr x,y,c)) \/ ((InputVertices (1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 )) \ (InnerVertices (BorrowIStr x,y,c))) by A2, FACIRC_1:6;
given xx being pair set such that A4: xx in InputVertices (BorrowStr x,y,c) ; :: according to FACIRC_1:def 2 :: thesis: contradiction
A5: InputVertices (1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 ) = {[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]} by FACIRC_1:42;
A6: ( InnerVertices (1GateCircStr <*x,y*>,and2a ) = {[<*x,y*>,and2a ]} & InnerVertices (1GateCircStr <*y,c*>,and2 ) = {[<*y,c*>,and2 ]} & InnerVertices (1GateCircStr <*x,c*>,and2a ) = {[<*x,c*>,and2a ]} ) by CIRCCOMB:49;
( 1GateCircStr <*x,y*>,and2a tolerates 1GateCircStr <*y,c*>,and2 & 1GateCircStr <*x,y*>,and2a tolerates 1GateCircStr <*x,c*>,and2a & 1GateCircStr <*y,c*>,and2 tolerates 1GateCircStr <*x,c*>,and2a ) by CIRCCOMB:55;
then A7: InnerVertices ((1GateCircStr <*x,y*>,and2a ) +* (1GateCircStr <*y,c*>,and2 )) = {[<*x,y*>,and2a ]} \/ {[<*y,c*>,and2 ]} by A6, CIRCCOMB:15;
(1GateCircStr <*x,y*>,and2a ) +* (1GateCircStr <*y,c*>,and2 ) tolerates 1GateCircStr <*x,c*>,and2a by CIRCCOMB:55;
then InnerVertices (BorrowIStr x,y,c) = ({[<*x,y*>,and2a ]} \/ {[<*y,c*>,and2 ]}) \/ {[<*x,c*>,and2a ]} by A6, A7, CIRCCOMB:15
.= {[<*x,y*>,and2a ],[<*y,c*>,and2 ]} \/ {[<*x,c*>,and2a ]} by ENUMSET1:41
.= {[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]} by ENUMSET1:43 ;
then (InputVertices (1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 )) \ (InnerVertices (BorrowIStr x,y,c)) = {} by A5, XBOOLE_1:37;
hence contradiction by A2, A3, A4, FACIRC_1:def 2; :: thesis: verum