let x, y, c be set ; ( 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*>,'&']
; 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*>,'&']
by FINSEQ_1:45;
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*>,'&']
by FINSEQ_1:45;
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*>,'&']
by FINSEQ_1:45;
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}
;
XBOOLE_0:def 10 {x,y,c} c= {x,y,c} \ {[<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3]}
let a be
object ;
TARSKI:def 3 ( 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}
;
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;
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}
; verum