let x, y, z be set ; :: thesis: ( x in the carrier of (GFA1CarryStr (x,y,z)) & y in the carrier of (GFA1CarryStr (x,y,z)) & z in the carrier of (GFA1CarryStr (x,y,z)) & [<*x,y*>,and2c] in the carrier of (GFA1CarryStr (x,y,z)) & [<*y,z*>,and2a] in the carrier of (GFA1CarryStr (x,y,z)) & [<*z,x*>,and2] in the carrier of (GFA1CarryStr (x,y,z)) & [<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3] in the carrier of (GFA1CarryStr (x,y,z)) )
set f1 = and2c ;
set f2 = and2a ;
set f3 = and2 ;
set f4 = or3 ;
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 Cxy = 1GateCircStr (<*x,y*>,and2c);
set Cyz = 1GateCircStr (<*y,z*>,and2a);
set Czx = 1GateCircStr (<*z,x*>,and2);
set Cxyz = 1GateCircStr (<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3);
set p = <*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>;
z in the carrier of (1GateCircStr (<*z,x*>,and2)) by FACIRC_1:43;
then A1: z in the carrier of (GFA1CarryIStr (x,y,z)) by FACIRC_1:20;
[<*z,x*>,and2] in the carrier of (1GateCircStr (<*z,x*>,and2)) by FACIRC_1:43;
then A2: [<*z,x*>,and2] in the carrier of (GFA1CarryIStr (x,y,z)) by FACIRC_1:20;
y in the carrier of (1GateCircStr (<*x,y*>,and2c)) by FACIRC_1:43;
then y in the carrier of ((1GateCircStr (<*x,y*>,and2c)) +* (1GateCircStr (<*y,z*>,and2a))) by FACIRC_1:20;
then A3: y in the carrier of (GFA1CarryIStr (x,y,z)) by FACIRC_1:20;
( the carrier of (1GateCircStr (<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3)) = (rng <*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>) \/ {[<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3]} & [<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3] in {[<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3]} ) by CIRCCOMB:def 6, TARSKI:def 1;
then A4: [<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3] in the carrier of (1GateCircStr (<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3)) by XBOOLE_0:def 3;
[<*y,z*>,and2a] in the carrier of (1GateCircStr (<*y,z*>,and2a)) by FACIRC_1:43;
then [<*y,z*>,and2a] in the carrier of ((1GateCircStr (<*x,y*>,and2c)) +* (1GateCircStr (<*y,z*>,and2a))) by FACIRC_1:20;
then A5: [<*y,z*>,and2a] in the carrier of (GFA1CarryIStr (x,y,z)) by FACIRC_1:20;
[<*x,y*>,and2c] in the carrier of (1GateCircStr (<*x,y*>,and2c)) by FACIRC_1:43;
then [<*x,y*>,and2c] in the carrier of ((1GateCircStr (<*x,y*>,and2c)) +* (1GateCircStr (<*y,z*>,and2a))) by FACIRC_1:20;
then A6: [<*x,y*>,and2c] in the carrier of (GFA1CarryIStr (x,y,z)) by FACIRC_1:20;
x in the carrier of (1GateCircStr (<*z,x*>,and2)) by FACIRC_1:43;
then x in the carrier of (GFA1CarryIStr (x,y,z)) by FACIRC_1:20;
hence ( x in the carrier of (GFA1CarryStr (x,y,z)) & y in the carrier of (GFA1CarryStr (x,y,z)) & z in the carrier of (GFA1CarryStr (x,y,z)) & [<*x,y*>,and2c] in the carrier of (GFA1CarryStr (x,y,z)) & [<*y,z*>,and2a] in the carrier of (GFA1CarryStr (x,y,z)) & [<*z,x*>,and2] in the carrier of (GFA1CarryStr (x,y,z)) & [<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3] in the carrier of (GFA1CarryStr (x,y,z)) ) by A3, A1, A6, A5, A2, A4, FACIRC_1:20; :: thesis: verum