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:42;
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:42
.= {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} by FINSEQ_2:128 ;
set BI = BorrowIStr (x,y,c);
assume that
A3: x <> [<*y,c*>,and2] and
A4: y <> [<*x,c*>,and2a] and
A5: c <> [<*x,y*>,and2a] ; :: thesis: InputVertices (BorrowStr (x,y,c)) = {x,y,c}
rng <*x,c*> = {x,c} by FINSEQ_2:127;
then A6: x in rng <*x,c*> by TARSKI:def 2;
len <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> = 3 by FINSEQ_1:45;
then A7: Seg 3 = dom <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> by FINSEQ_1:def 3;
then A8: 3 in dom <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> by FINSEQ_1:1;
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> . 3 = [<*x,c*>,and2a] ;
then [3,[<*x,c*>,and2a]] in <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> by A8, FUNCT_1:1;
then [<*x,c*>,and2a] in rng <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> by XTUPLE_0:def 13;
then A9: the_rank_of [<*x,c*>,and2a] in the_rank_of [<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3] by CLASSES1:82;
rng <*x,y*> = {x,y} by FINSEQ_2:127;
then A10: y in rng <*x,y*> by TARSKI:def 2;
A11: 1 in dom <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> by A7, FINSEQ_1:1;
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> . 1 = [<*x,y*>,and2a] ;
then [1,[<*x,y*>,and2a]] in <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> by A11, FUNCT_1:1;
then [<*x,y*>,and2a] in rng <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> by XTUPLE_0:def 13;
then A12: the_rank_of [<*x,y*>,and2a] in the_rank_of [<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3] by CLASSES1:82;
rng <*y,c*> = {y,c} by FINSEQ_2:127;
then A13: c in rng <*y,c*> by TARSKI:def 2;
A14: 2 in dom <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> by A7, FINSEQ_1:1;
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> . 2 = [<*y,c*>,and2] ;
then [2,[<*y,c*>,and2]] in <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> by A14, FUNCT_1:1;
then [<*y,c*>,and2] in rng <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> by XTUPLE_0:def 13;
then A15: the_rank_of [<*y,c*>,and2] in the_rank_of [<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3] by CLASSES1:82;
A16: {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} \ {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} = {} by XBOOLE_1:37;
A17: {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 object ; :: 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 A18: 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 A6, A9, A10, A12, A13, A15, CLASSES1:82;
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 A18, 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:5, CIRCCOMB:47
.= {x,y,c} \/ ({[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} \ (InnerVertices (BorrowIStr (x,y,c)))) by A1, A2, A3, A4, A5, A17, Th13
.= {x,y,c} \/ {} by A16, Th12
.= {x,y,c} ; :: thesis: verum