let x, y, z be set ; ( x in the carrier of (GFA3CarryStr x,y,z) & y in the carrier of (GFA3CarryStr x,y,z) & z in the carrier of (GFA3CarryStr x,y,z) & [<*x,y*>,and2b ] in the carrier of (GFA3CarryStr x,y,z) & [<*y,z*>,and2b ] in the carrier of (GFA3CarryStr x,y,z) & [<*z,x*>,and2b ] in the carrier of (GFA3CarryStr x,y,z) & [<*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ] in the carrier of (GFA3CarryStr x,y,z) )
set f1 = and2b ;
set f2 = and2b ;
set f3 = and2b ;
set f4 = nor3 ;
set xy = [<*x,y*>,and2b ];
set yz = [<*y,z*>,and2b ];
set zx = [<*z,x*>,and2b ];
set xyz = [<*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ];
set Cxy = 1GateCircStr <*x,y*>,and2b ;
set Cyz = 1GateCircStr <*y,z*>,and2b ;
set Czx = 1GateCircStr <*z,x*>,and2b ;
set Cxyz = 1GateCircStr <*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ;
set p = <*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>;
z in the carrier of (1GateCircStr <*z,x*>,and2b )
by FACIRC_1:43;
then A1:
z in the carrier of (GFA3CarryIStr x,y,z)
by FACIRC_1:20;
[<*z,x*>,and2b ] in the carrier of (1GateCircStr <*z,x*>,and2b )
by FACIRC_1:43;
then A2:
[<*z,x*>,and2b ] in the carrier of (GFA3CarryIStr x,y,z)
by FACIRC_1:20;
y in the carrier of (1GateCircStr <*x,y*>,and2b )
by FACIRC_1:43;
then
y in the carrier of ((1GateCircStr <*x,y*>,and2b ) +* (1GateCircStr <*y,z*>,and2b ))
by FACIRC_1:20;
then A3:
y in the carrier of (GFA3CarryIStr x,y,z)
by FACIRC_1:20;
( the carrier of (1GateCircStr <*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ) = (rng <*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>) \/ {[<*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ]} & [<*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ] in {[<*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ]} )
by CIRCCOMB:def 6, TARSKI:def 1;
then A4:
[<*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ] in the carrier of (1GateCircStr <*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 )
by XBOOLE_0:def 3;
[<*y,z*>,and2b ] in the carrier of (1GateCircStr <*y,z*>,and2b )
by FACIRC_1:43;
then
[<*y,z*>,and2b ] in the carrier of ((1GateCircStr <*x,y*>,and2b ) +* (1GateCircStr <*y,z*>,and2b ))
by FACIRC_1:20;
then A5:
[<*y,z*>,and2b ] in the carrier of (GFA3CarryIStr x,y,z)
by FACIRC_1:20;
[<*x,y*>,and2b ] in the carrier of (1GateCircStr <*x,y*>,and2b )
by FACIRC_1:43;
then
[<*x,y*>,and2b ] in the carrier of ((1GateCircStr <*x,y*>,and2b ) +* (1GateCircStr <*y,z*>,and2b ))
by FACIRC_1:20;
then A6:
[<*x,y*>,and2b ] in the carrier of (GFA3CarryIStr x,y,z)
by FACIRC_1:20;
x in the carrier of (1GateCircStr <*z,x*>,and2b )
by FACIRC_1:43;
then
x in the carrier of (GFA3CarryIStr x,y,z)
by FACIRC_1:20;
hence
( x in the carrier of (GFA3CarryStr x,y,z) & y in the carrier of (GFA3CarryStr x,y,z) & z in the carrier of (GFA3CarryStr x,y,z) & [<*x,y*>,and2b ] in the carrier of (GFA3CarryStr x,y,z) & [<*y,z*>,and2b ] in the carrier of (GFA3CarryStr x,y,z) & [<*z,x*>,and2b ] in the carrier of (GFA3CarryStr x,y,z) & [<*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ] in the carrier of (GFA3CarryStr x,y,z) )
by A3, A1, A6, A5, A2, A4, FACIRC_1:20; verum