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:42;
A2: InputVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)) = rng <*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*> by CIRCCOMB:42
.= {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} by FINSEQ_2:128 ;
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:127;
then A6: x in rng <*c,x*> by TARSKI:def 2;
len <*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*> = 3 by FINSEQ_1:45;
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:1;
<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*> . 3 = [<*c,x*>,'&'] ;
then [3,[<*c,x*>,'&']] in <*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*> by A8, FUNCT_1:1;
then [<*c,x*>,'&'] in rng <*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*> by XTUPLE_0:def 13;
then A9: the_rank_of [<*c,x*>,'&'] in the_rank_of [<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,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*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*> by A7, FINSEQ_1:1;
<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*> . 1 = [<*x,y*>,'&'] ;
then [1,[<*x,y*>,'&']] in <*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*> by A11, FUNCT_1:1;
then [<*x,y*>,'&'] in rng <*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*> by XTUPLE_0:def 13;
then A12: the_rank_of [<*x,y*>,'&'] in the_rank_of [<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,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*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*> by A7, FINSEQ_1:1;
<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*> . 2 = [<*y,c*>,'&'] ;
then [2,[<*y,c*>,'&']] in <*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*> by A14, FUNCT_1:1;
then [<*y,c*>,'&'] in rng <*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*> by XTUPLE_0:def 13;
then A15: the_rank_of [<*y,c*>,'&'] in the_rank_of [<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3] by CLASSES1:82;
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 object ; :: 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:82;
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:5, CIRCCOMB:47
.= {x,y,c} \/ ({[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} \ (InnerVertices (MajorityIStr (x,y,c)))) by A1, A2, A3, A4, A5, A17, Th18
.= {x,y,c} \/ {} by A16, Th17
.= {x,y,c} ; :: thesis: verum