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

proof

thus {x,y,c} \ {[<*[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]*>,or3 ]} c= {x,y,c} ; :: according to XBOOLE_0:def 10 :: thesis: {x,y,c} c= {x,y,c} \ {[<*[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]*>,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*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]*>,or3 ]} )
assume A18: a in {x,y,c} ; :: thesis: a in {x,y,c} \ {[<*[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]*>,or3 ]}
then ( a = x or a = y or a = c ) by ENUMSET1:def 1;
then a <> [<*[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]*>,or3 ] by A6, A9, A10, A12, A13, A15, CLASSES1:90;
then not a in {[<*[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]*>,or3 ]} by TARSKI:def 1;
hence a in {x,y,c} \ {[<*[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]*>,or3 ]} by A18, XBOOLE_0:def 5; :: thesis: verum

end;

thus InputVertices (MajorityStr x,y,c) = ((InputVertices (MajorityIStr x,y,c)) \ (InnerVertices (1GateCircStr <*[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]*>,or3 ))) \/ ((InputVertices (1GateCircStr <*[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]*>,or3 )) \ (InnerVertices (MajorityIStr x,y,c))) by CIRCCMB2:6, CIRCCOMB:55
.= {x,y,c} \/ ({[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]} \ (InnerVertices (MajorityIStr x,y,c))) by A1, A2, A3, A4, A5, A17, Th19
.= {x,y,c} \/ {} by A16, Th18
.= {x,y,c} ; :: thesis: verum