let x, y, c be object ; :: thesis: for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN st c <> [<*x,y*>,f] holds
InputVertices (2GatesCircStr (x,y,c,f)) = {x,y,c}
let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN; :: thesis: ( c <> [<*x,y*>,f] implies InputVertices (2GatesCircStr (x,y,c,f)) = {x,y,c} )
assume A1: c <> [<*x,y*>,f] ; :: thesis: InputVertices (2GatesCircStr (x,y,c,f)) = {x,y,c}
set S = 2GatesCircStr (x,y,c,f);
set S1 = 1GateCircStr (<*x,y*>,f);
set p = <*[<*x,y*>,f],c*>;
set S2 = 1GateCircStr (<*[<*x,y*>,f],c*>,f);
set R = the ResultSort of (2GatesCircStr (x,y,c,f));
A2: the carrier of (2GatesCircStr (x,y,c,f)) = the carrier of (1GateCircStr (<*x,y*>,f)) \/ the carrier of (1GateCircStr (<*[<*x,y*>,f],c*>,f)) by CIRCCOMB:def 2;
A3: rng <*x,y*> = {x,y} by FINSEQ_2:127;
then A4: the carrier of (1GateCircStr (<*x,y*>,f)) = {x,y} \/ {[<*x,y*>,f]} by CIRCCOMB:def 6;
A5: rng the ResultSort of (2GatesCircStr (x,y,c,f)) = {[<*x,y*>,f],(2GatesCircOutput (x,y,c,f))} by Th56
.= {[<*x,y*>,f],[<*[<*x,y*>,f],c*>,f]} ;
A6: rng <*[<*x,y*>,f],c*> = {[<*x,y*>,f],c} by FINSEQ_2:127;
then A7: the carrier of (1GateCircStr (<*[<*x,y*>,f],c*>,f)) = {[<*x,y*>,f],c} \/ {[<*[<*x,y*>,f],c*>,f]} by CIRCCOMB:def 6;
thus InputVertices (2GatesCircStr (x,y,c,f)) c= {x,y,c} :: according to XBOOLE_0:def 10 :: thesis: {x,y,c} c= InputVertices (2GatesCircStr (x,y,c,f))

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in InputVertices (2GatesCircStr (x,y,c,f)) or z in {x,y,c} )
assume A8: z in InputVertices (2GatesCircStr (x,y,c,f)) ; :: thesis: z in {x,y,c}
then ( z in the carrier of (1GateCircStr (<*x,y*>,f)) or z in the carrier of (1GateCircStr (<*[<*x,y*>,f],c*>,f)) ) by A2, XBOOLE_0:def 3;
then ( z in {x,y} or z in {[<*x,y*>,f]} or z in {[<*x,y*>,f],c} or z in {[<*[<*x,y*>,f],c*>,f]} ) by A4, A7, XBOOLE_0:def 3;
then A9: ( z = x or z = y or z = [<*x,y*>,f] or z = c or z = [<*[<*x,y*>,f],c*>,f] ) by TARSKI:def 1, TARSKI:def 2;
not z in rng the ResultSort of (2GatesCircStr (x,y,c,f)) by A8, XBOOLE_0:def 5;
hence z in {x,y,c} by A5, A9, ENUMSET1:def 1, TARSKI:def 2; :: thesis: verum

end;

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in {x,y,c} or z in InputVertices (2GatesCircStr (x,y,c,f)) )
reconsider zz = z as set by TARSKI:1;
assume z in {x,y,c} ; :: thesis: z in InputVertices (2GatesCircStr (x,y,c,f))
then A10: ( z = x or z = y or z = c ) by ENUMSET1:def 1;
then ( z in {x,y} or z in rng <*[<*x,y*>,f],c*> ) by A6, TARSKI:def 2;
then ( z in InputVertices (1GateCircStr (<*x,y*>,f)) or z in InputVertices (1GateCircStr (<*[<*x,y*>,f],c*>,f)) ) by A3, CIRCCOMB:42;
then A11: z in the carrier of (2GatesCircStr (x,y,c,f)) by A2, XBOOLE_0:def 3;
( ( z in {x,y} & [<*x,y*>,f] in rng <*[<*x,y*>,f],c*> ) or z in {c} ) by A6, A10, TARSKI:def 1, TARSKI:def 2;
then A12: ( ( the_rank_of zz in the_rank_of [<*x,y*>,f] & the_rank_of [<*x,y*>,f] in the_rank_of [<*[<*x,y*>,f],c*>,f] ) or ( z = c & c in rng <*[<*x,y*>,f],c*> ) ) by A3, A6, CLASSES1:82, TARSKI:def 1, TARSKI:def 2;
then the_rank_of zz in the_rank_of [<*[<*x,y*>,f],c*>,f] by CLASSES1:82, ORDINAL1:10;
then A13: z <> [<*[<*x,y*>,f],c*>,f] ;
z <> [<*x,y*>,f] by A1, A12;
then not z in rng the ResultSort of (2GatesCircStr (x,y,c,f)) by A5, A13, TARSKI:def 2;
hence z in InputVertices (2GatesCircStr (x,y,c,f)) by A11, XBOOLE_0:def 5; :: thesis: verum