let x, y, c be set ; ( x <> [<*y,c*>,and2] & y <> [<*x,c*>,and2a] & c <> [<*x,y*>,and2a] implies InputVertices (BorrowStr (x,y,c)) = {x,y,c} )
set xy = [<*x,y*>,and2a];
set yc = [<*y,c*>,and2];
set xc = [<*x,c*>,and2a];
set S = 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3);
A1:
InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) = {[<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3]}
by CIRCCOMB:42;
A2: InputVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) =
rng <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>
by CIRCCOMB:42
.=
{[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]}
by FINSEQ_2:128
;
set BI = BorrowIStr (x,y,c);
assume that
A3:
x <> [<*y,c*>,and2]
and
A4:
y <> [<*x,c*>,and2a]
and
A5:
c <> [<*x,y*>,and2a]
; InputVertices (BorrowStr (x,y,c)) = {x,y,c}
rng <*x,c*> = {x,c}
by FINSEQ_2:127;
then A6:
x in rng <*x,c*>
by TARSKI:def 2;
len <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> = 3
by FINSEQ_1:45;
then A7:
Seg 3 = dom <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>
by FINSEQ_1:def 3;
then A8:
3 in dom <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>
by FINSEQ_1:1;
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> . 3 = [<*x,c*>,and2a]
by FINSEQ_1:45;
then
[3,[<*x,c*>,and2a]] in <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>
by A8, FUNCT_1:1;
then
[<*x,c*>,and2a] in rng <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>
by XTUPLE_0:def 13;
then A9:
the_rank_of [<*x,c*>,and2a] in the_rank_of [<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,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*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>
by A7, FINSEQ_1:1;
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> . 1 = [<*x,y*>,and2a]
by FINSEQ_1:45;
then
[1,[<*x,y*>,and2a]] in <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>
by A11, FUNCT_1:1;
then
[<*x,y*>,and2a] in rng <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>
by XTUPLE_0:def 13;
then A12:
the_rank_of [<*x,y*>,and2a] in the_rank_of [<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,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*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>
by A7, FINSEQ_1:1;
<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*> . 2 = [<*y,c*>,and2]
by FINSEQ_1:45;
then
[2,[<*y,c*>,and2]] in <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>
by A14, FUNCT_1:1;
then
[<*y,c*>,and2] in rng <*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>
by XTUPLE_0:def 13;
then A15:
the_rank_of [<*y,c*>,and2] in the_rank_of [<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3]
by CLASSES1:82;
A16:
{[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} \ {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} = {}
by XBOOLE_1:37;
A17:
{x,y,c} \ {[<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3]} = {x,y,c}
proof
thus
{x,y,c} \ {[<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3]} c= {x,y,c}
;
XBOOLE_0:def 10 {x,y,c} c= {x,y,c} \ {[<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3]}
let a be
object ;
TARSKI:def 3 ( not a in {x,y,c} or a in {x,y,c} \ {[<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3]} )
assume A18:
a in {x,y,c}
;
a in {x,y,c} \ {[<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3]}
then
(
a = x or
a = y or
a = c )
by ENUMSET1:def 1;
then
a <> [<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3]
by A6, A9, A10, A12, A13, A15, CLASSES1:82;
then
not
a in {[<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3]}
by TARSKI:def 1;
hence
a in {x,y,c} \ {[<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3]}
by A18, XBOOLE_0:def 5;
verum
end;
thus InputVertices (BorrowStr (x,y,c)) =
((InputVertices (BorrowIStr (x,y,c))) \ (InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)))) \/ ((InputVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) \ (InnerVertices (BorrowIStr (x,y,c))))
by CIRCCMB2:5, CIRCCOMB:47
.=
{x,y,c} \/ ({[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} \ (InnerVertices (BorrowIStr (x,y,c))))
by A1, A2, A3, A4, A5, A17, Th13
.=
{x,y,c} \/ {}
by A16, Th12
.=
{x,y,c}
; verum