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