set f1 = and2c ;
set f2 = and2a ;
set f3 = and2 ;
set f4 = or3 ;
let x, y, z be set ; :: thesis: ( x <> [<*y,z*>,and2a ] & y <> [<*z,x*>,and2 ] & z <> [<*x,y*>,and2c ] implies InputVertices (GFA1CarryStr x,y,z) = {x,y,z} )
set xy = [<*x,y*>,and2c ];
set yz = [<*y,z*>,and2a ];
set zx = [<*z,x*>,and2 ];
set xyz = [<*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 ];
set S = 1GateCircStr <*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 ;
set MI = GFA1CarryIStr x,y,z;
A1: InnerVertices (1GateCircStr <*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 ) = {[<*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 ]} by CIRCCOMB:49;
A2: InputVertices (1GateCircStr <*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 ) = rng <*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*> by CIRCCOMB:49
.= {[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]} by FINSEQ_2:148 ;
assume A3: ( x <> [<*y,z*>,and2a ] & y <> [<*z,x*>,and2 ] & z <> [<*x,y*>,and2c ] ) ; :: thesis: InputVertices (GFA1CarryStr x,y,z) = {x,y,z}
A4: {x,y,z} \ {[<*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 ]} = {x,y,z} by Lm2;
A5: {[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]} \ {[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]} = {} by XBOOLE_1:37;
thus InputVertices (GFA1CarryStr x,y,z) = ((InputVertices (GFA1CarryIStr x,y,z)) \ (InnerVertices (1GateCircStr <*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 ))) \/ ((InputVertices (1GateCircStr <*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 )) \ (InnerVertices (GFA1CarryIStr x,y,z))) by CIRCCMB2:6, CIRCCOMB:55
.= {x,y,z} \/ ({[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]} \ (InnerVertices (GFA1CarryIStr x,y,z))) by A1, A2, A3, A4, Th52
.= {x,y,z} \/ {} by A5, Th49
.= {x,y,z} ; :: thesis: verum