let x, y, c be set ; :: thesis: ( x <> [<*y,c*>,and2 ] & y <> [<*x,c*>,and2a ] & c <> [<*x,y*>,and2a ] implies InputVertices (BorrowStr x,y,c) = {x,y,c} )
set xy = [<*x,y*>,and2a ];
set yc = [<*y,c*>,and2 ];
set xc = [<*x,c*>,and2a ];
set S = 1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 ;
A1: InnerVertices (1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 ) = {[<*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 ]} by CIRCCOMB:49;
A2: InputVertices (1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 ) = rng <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*> by CIRCCOMB:49
.= {[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]} by FINSEQ_2:148 ;
set BI = BorrowIStr x,y,c;
assume A3: ( x <> [<*y,c*>,and2 ] & y <> [<*x,c*>,and2a ] & c <> [<*x,y*>,and2a ] ) ; :: thesis: InputVertices (BorrowStr x,y,c) = {x,y,c}
rng <*x,c*> = {x,c} by FINSEQ_2:147;
then A4: x in rng <*x,c*> by TARSKI:def 2;
len <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*> = 3 by FINSEQ_1:62;
then A5: Seg 3 = dom <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*> by FINSEQ_1:def 3;
then A6: 3 in dom <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*> by FINSEQ_1:3;
<*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*> . 3 = [<*x,c*>,and2a ] by FINSEQ_1:62;
then [3,[<*x,c*>,and2a ]] in <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*> by A6, FUNCT_1:8;
then [<*x,c*>,and2a ] in rng <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*> by RELAT_1:def 5;
then A7: the_rank_of [<*x,c*>,and2a ] in the_rank_of [<*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 ] by CLASSES1:90;
rng <*x,y*> = {x,y} by FINSEQ_2:147;
then A8: y in rng <*x,y*> by TARSKI:def 2;
A9: 1 in dom <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*> by A5, FINSEQ_1:3;
<*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*> . 1 = [<*x,y*>,and2a ] by FINSEQ_1:62;
then [1,[<*x,y*>,and2a ]] in <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*> by A9, FUNCT_1:8;
then [<*x,y*>,and2a ] in rng <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*> by RELAT_1:def 5;
then A10: the_rank_of [<*x,y*>,and2a ] in the_rank_of [<*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 ] by CLASSES1:90;
rng <*y,c*> = {y,c} by FINSEQ_2:147;
then A11: c in rng <*y,c*> by TARSKI:def 2;
A12: 2 in dom <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*> by A5, FINSEQ_1:3;
<*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*> . 2 = [<*y,c*>,and2 ] by FINSEQ_1:62;
then [2,[<*y,c*>,and2 ]] in <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*> by A12, FUNCT_1:8;
then [<*y,c*>,and2 ] in rng <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*> by RELAT_1:def 5;
then A13: the_rank_of [<*y,c*>,and2 ] in the_rank_of [<*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 ] by CLASSES1:90;
A14: {[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]} \ {[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]} = {} by XBOOLE_1:37;
A15: {x,y,c} \ {[<*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 ]} = {x,y,c}

proof

thus {x,y,c} \ {[<*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 ]} c= {x,y,c} ; :: according to XBOOLE_0:def 10 :: thesis: {x,y,c} c= {x,y,c} \ {[<*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 ]}
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in {x,y,c} or a in {x,y,c} \ {[<*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 ]} )
assume A16: a in {x,y,c} ; :: thesis: a in {x,y,c} \ {[<*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 ]}
then ( a = x or a = y or a = c ) by ENUMSET1:def 1;
then a <> [<*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 ] by A4, A7, A8, A10, A11, A13, CLASSES1:90;
then not a in {[<*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 ]} by TARSKI:def 1;
hence a in {x,y,c} \ {[<*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 ]} by A16, XBOOLE_0:def 5; :: thesis: verum

end;

thus InputVertices (BorrowStr x,y,c) = ((InputVertices (BorrowIStr x,y,c)) \ (InnerVertices (1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 ))) \/ ((InputVertices (1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 )) \ (InnerVertices (BorrowIStr x,y,c))) by CIRCCMB2:6, CIRCCOMB:55
.= {x,y,c} \/ ({[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]} \ (InnerVertices (BorrowIStr x,y,c))) by A1, A2, A3, A15, Th13
.= {x,y,c} \/ {} by A14, Th12
.= {x,y,c} ; :: thesis: verum