let c, x, y be set ; :: 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 p = <*[<*x,y*>,f],c*>;
set S1 = 1GateCircStr <*x,y*>,f;
set S2 = 1GateCircStr <*[<*x,y*>,f],c*>,f;
set S = 2GatesCircStr x,y,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 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]} ;
A4: rng <*x,y*> = {x,y} by FINSEQ_2:147;
then A5: the carrier of (1GateCircStr <*x,y*>,f) = {x,y} \/ {[<*x,y*>,f]} by CIRCCOMB:def 6;
A6: rng <*[<*x,y*>,f],c*> = {[<*x,y*>,f],c} by FINSEQ_2:147;
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 set ; :: 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 A9: ( z in the carrier of (2GatesCircStr x,y,c,f) & not z in rng the ResultSort of (2GatesCircStr x,y,c,f) ) by XBOOLE_0:def 5;
( z in the carrier of (1GateCircStr <*x,y*>,f) or z in the carrier of (1GateCircStr <*[<*x,y*>,f],c*>,f) ) by A2, A8, 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 A5, A7, XBOOLE_0:def 3;
then ( 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;
hence z in {x,y,c} by A3, A9, ENUMSET1:def 1, TARSKI:def 2; :: thesis: verum

end;

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in {x,y,c} or z in InputVertices (2GatesCircStr x,y,c,f) )
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} & [<*x,y*>,f] in rng <*[<*x,y*>,f],c*> ) or z in {c} ) by A6, TARSKI:def 1, TARSKI:def 2;
then ( ( the_rank_of z 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 A4, A6, CLASSES1:90, TARSKI:def 1, TARSKI:def 2;
then A11: ( the_rank_of z in the_rank_of [<*[<*x,y*>,f],c*>,f] & z <> [<*x,y*>,f] ) by A1, CLASSES1:90, ORDINAL1:19;
then z <> [<*[<*x,y*>,f],c*>,f] ;
then A12: not z in rng the ResultSort of (2GatesCircStr x,y,c,f) by A3, A11, TARSKI:def 2;
( z in {x,y} or z in rng <*[<*x,y*>,f],c*> ) by A6, A10, TARSKI:def 2;
then ( z in InputVertices (1GateCircStr <*x,y*>,f) or z in InputVertices (1GateCircStr <*[<*x,y*>,f],c*>,f) ) by A4, CIRCCOMB:49;
then z in the carrier of (2GatesCircStr x,y,c,f) by A2, XBOOLE_0:def 3;
hence z in InputVertices (2GatesCircStr x,y,c,f) by A12, XBOOLE_0:def 5; :: thesis: verum