theorem Th43: :: FACIRC_1:43

for x, y, f being object holds
( 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)) )