let x, y, z, f be object ; ( 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; verum