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