let x, y, z, f be object ; :: thesis: ( x in the carrier of (1GateCircStr (<*x,y,z*>,f)) & y in the carrier of (1GateCircStr (<*x,y,z*>,f)) & z in the carrier of (1GateCircStr (<*x,y,z*>,f)) )
set p = <*x,y,z*>;
set A = the carrier of (1GateCircStr (<*x,y,z*>,f));
y in {x,y,z} by ENUMSET1:def 1;
then A1: y in rng <*x,y,z*> by FINSEQ_2:128;
z in {x,y,z} by ENUMSET1:def 1;
then A2: z in rng <*x,y,z*> by FINSEQ_2:128;
x in {x,y,z} by ENUMSET1:def 1;
then ( the carrier of (1GateCircStr (<*x,y,z*>,f)) = (rng <*x,y,z*>) \/ {[<*x,y,z*>,f]} & x in rng <*x,y,z*> ) by CIRCCOMB:def 6, FINSEQ_2:128;
hence ( x in the carrier of (1GateCircStr (<*x,y,z*>,f)) & y in the carrier of (1GateCircStr (<*x,y,z*>,f)) & z in the carrier of (1GateCircStr (<*x,y,z*>,f)) ) by A1, A2, XBOOLE_0:def 3; :: thesis: verum