theorem Th10: :: CIRCCMB2:10
for S1, S2, S being non empty non void Circuit-like ManySortedSign st InputVertices S1 misses InnerVertices S2 & S = S1 +* S2 holds
for C1 being non-empty Circuit of S1
for C2 being non-empty Circuit of S2
for C being non-empty Circuit of S st C1 tolerates C2 & C = C1 +* C2 holds
for s1 being State of C1
for s being State of C st s1 = s | the carrier of S1 holds
Following s1 = (Following s) | the carrier of S1