let x, y, c be set ; :: thesis: ( x <> [<*y,c*>,and2 ] & y <> [<*x,c*>,and2a ] & c <> [<*x,y*>,and2a ] implies InputVertices (BorrowIStr x,y,c) = {x,y,c} )
assume that
A1: x <> [<*y,c*>,and2 ] and
A2: y <> [<*x,c*>,and2a ] and
A3: c <> [<*x,y*>,and2a ] ; :: thesis: InputVertices (BorrowIStr x,y,c) = {x,y,c}
A4: 1GateCircStr <*x,y*>,and2a tolerates 1GateCircStr <*y,c*>,and2 by CIRCCOMB:55;
A5: y in {1,y} by TARSKI:def 2;
A6: y in {2,y} by TARSKI:def 2;
A7: {1,y} in [1,y] by TARSKI:def 2;
A8: {2,y} in [2,y] by TARSKI:def 2;
<*y,c*> = <*y*> ^ <*c*> by FINSEQ_1:def 9;
then A9: <*y*> c= <*y,c*> by FINSEQ_6:12;
<*y*> = {[1,y]} by FINSEQ_1:def 5;
then A10: [1,y] in <*y*> by TARSKI:def 1;
A11: <*y,c*> in {<*y,c*>} by TARSKI:def 1;
A12: {<*y,c*>} in [<*y,c*>,and2 ] by TARSKI:def 2;
then A13: y <> [<*y,c*>,and2 ] by A5, A7, A9, A10, A11, ORDINAL1:5;
A14: c in {2,c} by TARSKI:def 2;
A15: {2,c} in [2,c] by TARSKI:def 2;
dom <*y,c*> = Seg 2 by FINSEQ_1:110;
then A18: 2 in dom <*y,c*> by FINSEQ_1:3;
<*y,c*> . 2 = c by FINSEQ_1:61;
then [2,c] in <*y,c*> by A18, FUNCT_1:8;
then A19: c <> [<*y,c*>,and2 ] by A11, A12, A14, A15, ORDINAL1:5;
dom <*x,y*> = Seg 2 by FINSEQ_1:110;
then A22: 2 in dom <*x,y*> by FINSEQ_1:3;
<*x,y*> . 2 = y by FINSEQ_1:61;
then A23: [2,y] in <*x,y*> by A22, FUNCT_1:8;
A24: <*x,y*> in {<*x,y*>} by TARSKI:def 1;
{<*x,y*>} in [<*x,y*>,and2a ] by TARSKI:def 2;
then y <> [<*x,y*>,and2a ] by A6, A8, A23, A24, ORDINAL1:5;
then A25: not [<*x,y*>,and2a ] in {y,c} by A3, TARSKI:def 2;
A26: x in {1,x} by TARSKI:def 2;
A27: {1,x} in [1,x] by TARSKI:def 2;
<*x,y*> = <*x*> ^ <*y*> by FINSEQ_1:def 9;
then A28: <*x*> c= <*x,y*> by FINSEQ_6:12;
<*x*> = {[1,x]} by FINSEQ_1:def 5;
then A29: [1,x] in <*x*> by TARSKI:def 1;
A30: <*x,y*> in {<*x,y*>} by TARSKI:def 1;
{<*x,y*>} in [<*x,y*>,and2a ] by TARSKI:def 2;
then A31: x <> [<*x,y*>,and2a ] by A26, A27, A28, A29, A30, ORDINAL1:5;
A32: not c in {[<*x,y*>,and2a ],[<*y,c*>,and2 ]} by A3, A19, TARSKI:def 2;
A33: not x in {[<*x,y*>,and2a ],[<*y,c*>,and2 ]} by A1, A31, TARSKI:def 2;
A34: c in {2,c} by TARSKI:def 2;
A35: {2,c} in [2,c] by TARSKI:def 2;
dom <*x,c*> = Seg 2 by FINSEQ_1:110;
then A38: 2 in dom <*x,c*> by FINSEQ_1:3;
<*x,c*> . 2 = c by FINSEQ_1:61;
then A39: [2,c] in <*x,c*> by A38, FUNCT_1:8;
A40: <*x,c*> in {<*x,c*>} by TARSKI:def 1;
{<*x,c*>} in [<*x,c*>,and2a ] by TARSKI:def 2;
then A41: c <> [<*x,c*>,and2a ] by A34, A35, A39, A40, ORDINAL1:5;
A42: x in {1,x} by TARSKI:def 2;
A43: {1,x} in [1,x] by TARSKI:def 2;
<*x,c*> = <*x*> ^ <*c*> by FINSEQ_1:def 9;
then A44: <*x*> c= <*x,c*> by FINSEQ_6:12;
<*x*> = {[1,x]} by FINSEQ_1:def 5;
then A45: [1,x] in <*x*> by TARSKI:def 1;
A46: <*x,c*> in {<*x,c*>} by TARSKI:def 1;
{<*x,c*>} in [<*x,c*>,and2a ] by TARSKI:def 2;
then x <> [<*x,c*>,and2a ] by A42, A43, A44, A45, A46, ORDINAL1:5;
then A47: not [<*x,c*>,and2a ] in {x,y,c} by A2, A41, ENUMSET1:def 1;
InputVertices (BorrowIStr x,y,c) = ((InputVertices ((1GateCircStr <*x,y*>,and2a ) +* (1GateCircStr <*y,c*>,and2 ))) \ (InnerVertices (1GateCircStr <*x,c*>,and2a ))) \/ ((InputVertices (1GateCircStr <*x,c*>,and2a )) \ (InnerVertices ((1GateCircStr <*x,y*>,and2a ) +* (1GateCircStr <*y,c*>,and2 )))) by CIRCCMB2:6, CIRCCOMB:55
.= ((((InputVertices (1GateCircStr <*x,y*>,and2a )) \ (InnerVertices (1GateCircStr <*y,c*>,and2 ))) \/ ((InputVertices (1GateCircStr <*y,c*>,and2 )) \ (InnerVertices (1GateCircStr <*x,y*>,and2a )))) \ (InnerVertices (1GateCircStr <*x,c*>,and2a ))) \/ ((InputVertices (1GateCircStr <*x,c*>,and2a )) \ (InnerVertices ((1GateCircStr <*x,y*>,and2a ) +* (1GateCircStr <*y,c*>,and2 )))) by CIRCCMB2:6, CIRCCOMB:55
.= ((((InputVertices (1GateCircStr <*x,y*>,and2a )) \ (InnerVertices (1GateCircStr <*y,c*>,and2 ))) \/ ((InputVertices (1GateCircStr <*y,c*>,and2 )) \ (InnerVertices (1GateCircStr <*x,y*>,and2a )))) \ (InnerVertices (1GateCircStr <*x,c*>,and2a ))) \/ ((InputVertices (1GateCircStr <*x,c*>,and2a )) \ ((InnerVertices (1GateCircStr <*x,y*>,and2a )) \/ (InnerVertices (1GateCircStr <*y,c*>,and2 )))) by A4, CIRCCOMB:15
.= ((((InputVertices (1GateCircStr <*x,y*>,and2a )) \ {[<*y,c*>,and2 ]}) \/ ((InputVertices (1GateCircStr <*y,c*>,and2 )) \ (InnerVertices (1GateCircStr <*x,y*>,and2a )))) \ (InnerVertices (1GateCircStr <*x,c*>,and2a ))) \/ ((InputVertices (1GateCircStr <*x,c*>,and2a )) \ ((InnerVertices (1GateCircStr <*x,y*>,and2a )) \/ (InnerVertices (1GateCircStr <*y,c*>,and2 )))) by CIRCCOMB:49
.= ((((InputVertices (1GateCircStr <*x,y*>,and2a )) \ {[<*y,c*>,and2 ]}) \/ ((InputVertices (1GateCircStr <*y,c*>,and2 )) \ {[<*x,y*>,and2a ]})) \ (InnerVertices (1GateCircStr <*x,c*>,and2a ))) \/ ((InputVertices (1GateCircStr <*x,c*>,and2a )) \ ((InnerVertices (1GateCircStr <*x,y*>,and2a )) \/ (InnerVertices (1GateCircStr <*y,c*>,and2 )))) by CIRCCOMB:49
.= ((((InputVertices (1GateCircStr <*x,y*>,and2a )) \ {[<*y,c*>,and2 ]}) \/ ((InputVertices (1GateCircStr <*y,c*>,and2 )) \ {[<*x,y*>,and2a ]})) \ {[<*x,c*>,and2a ]}) \/ ((InputVertices (1GateCircStr <*x,c*>,and2a )) \ ((InnerVertices (1GateCircStr <*x,y*>,and2a )) \/ (InnerVertices (1GateCircStr <*y,c*>,and2 )))) by CIRCCOMB:49
.= ((((InputVertices (1GateCircStr <*x,y*>,and2a )) \ {[<*y,c*>,and2 ]}) \/ ((InputVertices (1GateCircStr <*y,c*>,and2 )) \ {[<*x,y*>,and2a ]})) \ {[<*x,c*>,and2a ]}) \/ ((InputVertices (1GateCircStr <*x,c*>,and2a )) \ ({[<*x,y*>,and2a ]} \/ (InnerVertices (1GateCircStr <*y,c*>,and2 )))) by CIRCCOMB:49
.= ((((InputVertices (1GateCircStr <*x,y*>,and2a )) \ {[<*y,c*>,and2 ]}) \/ ((InputVertices (1GateCircStr <*y,c*>,and2 )) \ {[<*x,y*>,and2a ]})) \ {[<*x,c*>,and2a ]}) \/ ((InputVertices (1GateCircStr <*x,c*>,and2a )) \ ({[<*x,y*>,and2a ]} \/ {[<*y,c*>,and2 ]})) by CIRCCOMB:49
.= ((({x,y} \ {[<*y,c*>,and2 ]}) \/ ((InputVertices (1GateCircStr <*y,c*>,and2 )) \ {[<*x,y*>,and2a ]})) \ {[<*x,c*>,and2a ]}) \/ ((InputVertices (1GateCircStr <*x,c*>,and2a )) \ ({[<*x,y*>,and2a ]} \/ {[<*y,c*>,and2 ]})) by FACIRC_1:40
.= ((({x,y} \ {[<*y,c*>,and2 ]}) \/ ({y,c} \ {[<*x,y*>,and2a ]})) \ {[<*x,c*>,and2a ]}) \/ ((InputVertices (1GateCircStr <*x,c*>,and2a )) \ ({[<*x,y*>,and2a ]} \/ {[<*y,c*>,and2 ]})) by FACIRC_1:40
.= ((({x,y} \ {[<*y,c*>,and2 ]}) \/ ({y,c} \ {[<*x,y*>,and2a ]})) \ {[<*x,c*>,and2a ]}) \/ ({x,c} \ ({[<*x,y*>,and2a ]} \/ {[<*y,c*>,and2 ]})) by FACIRC_1:40
.= ((({x,y} \ {[<*y,c*>,and2 ]}) \/ ({y,c} \ {[<*x,y*>,and2a ]})) \ {[<*x,c*>,and2a ]}) \/ ({x,c} \ {[<*x,y*>,and2a ],[<*y,c*>,and2 ]}) by ENUMSET1:41
.= (({x,y} \/ ({y,c} \ {[<*x,y*>,and2a ]})) \ {[<*x,c*>,and2a ]}) \/ ({x,c} \ {[<*x,y*>,and2a ],[<*y,c*>,and2 ]}) by A1, A13, FACIRC_2:1
.= (({x,y} \/ {y,c}) \ {[<*x,c*>,and2a ]}) \/ ({x,c} \ {[<*x,y*>,and2a ],[<*y,c*>,and2 ]}) by A25, ZFMISC_1:65
.= (({x,y} \/ {y,c}) \ {[<*x,c*>,and2a ]}) \/ {x,c} by A32, A33, ZFMISC_1:72
.= ({x,y,y,c} \ {[<*x,c*>,and2a ]}) \/ {x,c} by ENUMSET1:45
.= ({y,y,x,c} \ {[<*x,c*>,and2a ]}) \/ {x,c} by ENUMSET1:110
.= ({y,x,c} \ {[<*x,c*>,and2a ]}) \/ {x,c} by ENUMSET1:71
.= ({x,y,c} \ {[<*x,c*>,and2a ]}) \/ {x,c} by ENUMSET1:99
.= {x,y,c} \/ {x,c} by A47, ZFMISC_1:65
.= {x,y,c,c,x} by ENUMSET1:49
.= {x,y,c,c} \/ {x} by ENUMSET1:50
.= {c,c,x,y} \/ {x} by ENUMSET1:118
.= {c,x,y} \/ {x} by ENUMSET1:71
.= {c,x,y,x} by ENUMSET1:46
.= {x,x,y,c} by ENUMSET1:113
.= {x,y,c} by ENUMSET1:71 ;
hence InputVertices (BorrowIStr x,y,c) = {x,y,c} ; :: thesis: verum