set f1 = and2c ;
set f2 = and2a ;
set f3 = and2 ;
set f4 = or3 ;
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 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 ;
y in the carrier of (1GateCircStr <*x,y*>,and2c ) by FACIRC_1:43;
then A1: y in the carrier of ((1GateCircStr <*x,y*>,and2c ) +* (1GateCircStr <*y,z*>,and2a )) by FACIRC_1:20;
( x in the carrier of (1GateCircStr <*z,x*>,and2 ) & z in the carrier of (1GateCircStr <*z,x*>,and2 ) ) by FACIRC_1:43;
then A2: ( x in the carrier of (GFA1CarryIStr x,y,z) & y in the carrier of (GFA1CarryIStr x,y,z) & z in the carrier of (GFA1CarryIStr x,y,z) ) by A1, FACIRC_1:20;
( [<*x,y*>,and2c ] in the carrier of (1GateCircStr <*x,y*>,and2c ) & [<*y,z*>,and2a ] in the carrier of (1GateCircStr <*y,z*>,and2a ) ) by FACIRC_1:43;
then A3: ( [<*x,y*>,and2c ] in the carrier of ((1GateCircStr <*x,y*>,and2c ) +* (1GateCircStr <*y,z*>,and2a )) & [<*y,z*>,and2a ] in the carrier of ((1GateCircStr <*x,y*>,and2c ) +* (1GateCircStr <*y,z*>,and2a )) ) by FACIRC_1:20;
[<*z,x*>,and2 ] in the carrier of (1GateCircStr <*z,x*>,and2 ) by FACIRC_1:43;
then A4: ( [<*x,y*>,and2c ] in the carrier of (GFA1CarryIStr x,y,z) & [<*y,z*>,and2a ] in the carrier of (GFA1CarryIStr x,y,z) & [<*z,x*>,and2 ] in the carrier of (GFA1CarryIStr x,y,z) ) by A3, FACIRC_1:20;
set p = <*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>;
( 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 [<*[<*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;
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 A2, A4, FACIRC_1:20; :: thesis: verum