let x, y, z, f be set ; :: 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);
( x in {x,y,z} & y in {x,y,z} & z 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*> & y in rng <*x,y,z*> & z in rng <*x,y,z*> ) by CIRCCOMB:def 6, FINSEQ_2:148;
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 XBOOLE_0:def 3; :: thesis: verum