let x, y, c be set ; :: thesis:
assume A1: ( x <> [<*y,c*>,'&' ] & y <> [<*c,x*>,'&' ] & c <> [<*x,y*>,'&' ] ) ; :: thesis:
A2: 1GateCircStr <*x,y*>,'&' tolerates 1GateCircStr <*y,c*>,'&' by CIRCCOMB:55;
A3: ( y in {1,y} & y in {2,y} ) by TARSKI:def 2;
A4: ( {1,y} in [1,y] & {2,y} in [2,y] ) by TARSKI:def 2;
<*y,c*> = <*y*> ^ <*c*> by FINSEQ_1:def 9;
then A5: <*y*> c= <*y,c*> by FINSEQ_6:12;
<*y*> = {[1,y]} by FINSEQ_1:def 5;
then A6: [1,y] in <*y*> by TARSKI:def 1;
A7: ( <*y,c*> in {<*y,c*>} & {<*y,c*>} in [<*y,c*>,'&' ] ) by TARSKI:def 1, TARSKI:def 2;
then A8: y <> [<*y,c*>,'&' ] by A3, A4, A5, A6, ORDINAL1:5;
A9: c in {2,c} by TARSKI:def 2;
A10: {2,c} in [2,c] by TARSKI:def 2;
( 2 in dom <*y,c*> & <*y,c*> . 2 = c )

dom <*y*> = Seg 1 by FINSEQ_1:def 8;
then A11: len <*y*> = 1 by FINSEQ_1:def 3;
dom <*c*> = Seg 1 by FINSEQ_1:def 8;
then A12: len <*c*> = 1 by FINSEQ_1:def 3;
dom <*y,c*> = dom (<*y*> ^ <*c*>) by FINSEQ_1:def 9
.= Seg 2 by A11, A12, FINSEQ_1:def 7 ;
hence ( 2 in dom <*y,c*> & <*y,c*> . 2 = c ) by FINSEQ_1:3, FINSEQ_1:61; :: thesis:

end;

then [2,c] in <*y,c*> by FUNCT_1:8;
then A13: c <> [<*y,c*>,'&' ] by A7, A9, A10, ORDINAL1:5;
( 2 in dom <*x,y*> & <*x,y*> . 2 = y )

dom <*x*> = Seg 1 by FINSEQ_1:def 8;
then A14: len <*x*> = 1 by FINSEQ_1:def 3;
dom <*y*> = Seg 1 by FINSEQ_1:def 8;
then A15: len <*y*> = 1 by FINSEQ_1:def 3;
dom <*x,y*> = dom (<*x*> ^ <*y*>) by FINSEQ_1:def 9
.= Seg 2 by A14, A15, FINSEQ_1:def 7 ;
hence ( 2 in dom <*x,y*> & <*x,y*> . 2 = y ) by FINSEQ_1:3, FINSEQ_1:61; :: thesis:

end;

then A16: [2,y] in <*x,y*> by FUNCT_1:8;
( <*x,y*> in {<*x,y*>} & {<*x,y*>} in [<*x,y*>,'&' ] ) by TARSKI:def 1, TARSKI:def 2;
then y <> [<*x,y*>,'&' ] by A3, A4, A16, ORDINAL1:5;
then A17: not [<*x,y*>,'&' ] in {y,c} by A1, TARSKI:def 2;
A18: x in {1,x} by TARSKI:def 2;
A19: {1,x} in [1,x] by TARSKI:def 2;
<*x,y*> = <*x*> ^ <*y*> by FINSEQ_1:def 9;
then A20: <*x*> c= <*x,y*> by FINSEQ_6:12;
<*x*> = {[1,x]} by FINSEQ_1:def 5;
then A21: [1,x] in <*x*> by TARSKI:def 1;
( <*x,y*> in {<*x,y*>} & {<*x,y*>} in [<*x,y*>,'&' ] ) by TARSKI:def 1, TARSKI:def 2;
then x <> [<*x,y*>,'&' ] by A18, A19, A20, A21, ORDINAL1:5;
then A22: ( not c in {[<*x,y*>,'&' ],[<*y,c*>,'&' ]} & not x in {[<*x,y*>,'&' ],[<*y,c*>,'&' ]} ) by A1, A13, TARSKI:def 2;
A23: x in {2,x} by TARSKI:def 2;
A24: {2,x} in [2,x] by TARSKI:def 2;
( 2 in dom <*c,x*> & <*c,x*> . 2 = x )

dom <*c*> = Seg 1 by FINSEQ_1:def 8;
then A25: len <*c*> = 1 by FINSEQ_1:def 3;
dom <*x*> = Seg 1 by FINSEQ_1:def 8;
then A26: len <*x*> = 1 by FINSEQ_1:def 3;
dom <*c,x*> = dom (<*c*> ^ <*x*>) by FINSEQ_1:def 9
.= Seg 2 by A25, A26, FINSEQ_1:def 7 ;
hence ( 2 in dom <*c,x*> & <*c,x*> . 2 = x ) by FINSEQ_1:3, FINSEQ_1:61; :: thesis:

end;

then A27: [2,x] in <*c,x*> by FUNCT_1:8;
( <*c,x*> in {<*c,x*>} & {<*c,x*>} in [<*c,x*>,'&' ] ) by TARSKI:def 1, TARSKI:def 2;
then A28: x <> [<*c,x*>,'&' ] by A23, A24, A27, ORDINAL1:5;
A29: c in {1,c} by TARSKI:def 2;
A30: {1,c} in [1,c] by TARSKI:def 2;
<*c,x*> = <*c*> ^ <*x*> by FINSEQ_1:def 9;
then A31: <*c*> c= <*c,x*> by FINSEQ_6:12;
<*c*> = {[1,c]} by FINSEQ_1:def 5;
then A32: [1,c] in <*c*> by TARSKI:def 1;
( <*c,x*> in {<*c,x*>} & {<*c,x*>} in [<*c,x*>,'&' ] ) by TARSKI:def 1, TARSKI:def 2;
then c <> [<*c,x*>,'&' ] by A29, A30, A31, A32, ORDINAL1:5;
then A33: not [<*c,x*>,'&' ] in {x,y,c} by A1, A28, ENUMSET1:def 1;
InputVertices (MajorityIStr x,y,c) = ((InputVertices ((1GateCircStr <*x,y*>,'&' ) +* (1GateCircStr <*y,c*>,'&' ))) \ (InnerVertices (1GateCircStr <*c,x*>,'&' ))) \/ ((InputVertices (1GateCircStr <*c,x*>,'&' )) \ (InnerVertices ((1GateCircStr <*x,y*>,'&' ) +* (1GateCircStr <*y,c*>,'&' )))) by CIRCCMB2:6, CIRCCOMB:55
.= ((((InputVertices (1GateCircStr <*x,y*>,'&' )) \ (InnerVertices (1GateCircStr <*y,c*>,'&' ))) \/ ((InputVertices (1GateCircStr <*y,c*>,'&' )) \ (InnerVertices (1GateCircStr <*x,y*>,'&' )))) \ (InnerVertices (1GateCircStr <*c,x*>,'&' ))) \/ ((InputVertices (1GateCircStr <*c,x*>,'&' )) \ (InnerVertices ((1GateCircStr <*x,y*>,'&' ) +* (1GateCircStr <*y,c*>,'&' )))) by CIRCCMB2:6, CIRCCOMB:55
.= ((((InputVertices (1GateCircStr <*x,y*>,'&' )) \ (InnerVertices (1GateCircStr <*y,c*>,'&' ))) \/ ((InputVertices (1GateCircStr <*y,c*>,'&' )) \ (InnerVertices (1GateCircStr <*x,y*>,'&' )))) \ (InnerVertices (1GateCircStr <*c,x*>,'&' ))) \/ ((InputVertices (1GateCircStr <*c,x*>,'&' )) \ ((InnerVertices (1GateCircStr <*x,y*>,'&' )) \/ (InnerVertices (1GateCircStr <*y,c*>,'&' )))) by A2, CIRCCOMB:15
.= ((((InputVertices (1GateCircStr <*x,y*>,'&' )) \ {[<*y,c*>,'&' ]}) \/ ((InputVertices (1GateCircStr <*y,c*>,'&' )) \ (InnerVertices (1GateCircStr <*x,y*>,'&' )))) \ (InnerVertices (1GateCircStr <*c,x*>,'&' ))) \/ ((InputVertices (1GateCircStr <*c,x*>,'&' )) \ ((InnerVertices (1GateCircStr <*x,y*>,'&' )) \/ (InnerVertices (1GateCircStr <*y,c*>,'&' )))) by CIRCCOMB:49
.= ((((InputVertices (1GateCircStr <*x,y*>,'&' )) \ {[<*y,c*>,'&' ]}) \/ ((InputVertices (1GateCircStr <*y,c*>,'&' )) \ {[<*x,y*>,'&' ]})) \ (InnerVertices (1GateCircStr <*c,x*>,'&' ))) \/ ((InputVertices (1GateCircStr <*c,x*>,'&' )) \ ((InnerVertices (1GateCircStr <*x,y*>,'&' )) \/ (InnerVertices (1GateCircStr <*y,c*>,'&' )))) by CIRCCOMB:49
.= ((((InputVertices (1GateCircStr <*x,y*>,'&' )) \ {[<*y,c*>,'&' ]}) \/ ((InputVertices (1GateCircStr <*y,c*>,'&' )) \ {[<*x,y*>,'&' ]})) \ {[<*c,x*>,'&' ]}) \/ ((InputVertices (1GateCircStr <*c,x*>,'&' )) \ ((InnerVertices (1GateCircStr <*x,y*>,'&' )) \/ (InnerVertices (1GateCircStr <*y,c*>,'&' )))) by CIRCCOMB:49
.= ((((InputVertices (1GateCircStr <*x,y*>,'&' )) \ {[<*y,c*>,'&' ]}) \/ ((InputVertices (1GateCircStr <*y,c*>,'&' )) \ {[<*x,y*>,'&' ]})) \ {[<*c,x*>,'&' ]}) \/ ((InputVertices (1GateCircStr <*c,x*>,'&' )) \ ({[<*x,y*>,'&' ]} \/ (InnerVertices (1GateCircStr <*y,c*>,'&' )))) by CIRCCOMB:49
.= ((((InputVertices (1GateCircStr <*x,y*>,'&' )) \ {[<*y,c*>,'&' ]}) \/ ((InputVertices (1GateCircStr <*y,c*>,'&' )) \ {[<*x,y*>,'&' ]})) \ {[<*c,x*>,'&' ]}) \/ ((InputVertices (1GateCircStr <*c,x*>,'&' )) \ ({[<*x,y*>,'&' ]} \/ {[<*y,c*>,'&' ]})) by CIRCCOMB:49
.= ((({x,y} \ {[<*y,c*>,'&' ]}) \/ ((InputVertices (1GateCircStr <*y,c*>,'&' )) \ {[<*x,y*>,'&' ]})) \ {[<*c,x*>,'&' ]}) \/ ((InputVertices (1GateCircStr <*c,x*>,'&' )) \ ({[<*x,y*>,'&' ]} \/ {[<*y,c*>,'&' ]})) by FACIRC_1:40
.= ((({x,y} \ {[<*y,c*>,'&' ]}) \/ ({y,c} \ {[<*x,y*>,'&' ]})) \ {[<*c,x*>,'&' ]}) \/ ((InputVertices (1GateCircStr <*c,x*>,'&' )) \ ({[<*x,y*>,'&' ]} \/ {[<*y,c*>,'&' ]})) by FACIRC_1:40
.= ((({x,y} \ {[<*y,c*>,'&' ]}) \/ ({y,c} \ {[<*x,y*>,'&' ]})) \ {[<*c,x*>,'&' ]}) \/ ({c,x} \ ({[<*x,y*>,'&' ]} \/ {[<*y,c*>,'&' ]})) by FACIRC_1:40
.= ((({x,y} \ {[<*y,c*>,'&' ]}) \/ ({y,c} \ {[<*x,y*>,'&' ]})) \ {[<*c,x*>,'&' ]}) \/ ({c,x} \ {[<*x,y*>,'&' ],[<*y,c*>,'&' ]}) by ENUMSET1:41
.= (({x,y} \/ ({y,c} \ {[<*x,y*>,'&' ]})) \ {[<*c,x*>,'&' ]}) \/ ({c,x} \ {[<*x,y*>,'&' ],[<*y,c*>,'&' ]}) by A1, A8, Th1
.= (({x,y} \/ {y,c}) \ {[<*c,x*>,'&' ]}) \/ ({c,x} \ {[<*x,y*>,'&' ],[<*y,c*>,'&' ]}) by A17, ZFMISC_1:65
.= (({x,y} \/ {y,c}) \ {[<*c,x*>,'&' ]}) \/ {c,x} by A22, ZFMISC_1:72
.= ({x,y,y,c} \ {[<*c,x*>,'&' ]}) \/ {c,x} by ENUMSET1:45
.= ({y,y,x,c} \ {[<*c,x*>,'&' ]}) \/ {c,x} by ENUMSET1:110
.= ({y,x,c} \ {[<*c,x*>,'&' ]}) \/ {c,x} by ENUMSET1:71
.= ({x,y,c} \ {[<*c,x*>,'&' ]}) \/ {c,x} by ENUMSET1:99
.= {x,y,c} \/ {c,x} by A33, 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 (MajorityIStr x,y,c) = {x,y,c} ; :: thesis: