let x, y, f be set ; :: 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} & y in {x,y} ) by TARSKI:def 2;
then ( the carrier of (1GateCircStr <*x,y*>,f) = (rng <*x,y*>) \/ {[<*x,y*>,f]} & x in rng <*x,y*> & y in rng <*x,y*> & [<*x,y*>,f] in {[<*x,y*>,f]} ) by CIRCCOMB:def 6, FINSEQ_2:147, 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 XBOOLE_0:def 3; :: thesis: verum