:: deftheorem Def10 defines CatCycles GRAPH_3:def 10 :
for G being Graph
for c1, c2 being Element of G -CycleSet st G -VSet (rng c1) meets G -VSet (rng c2) & rng c1 misses rng c2 holds
for b₄ being Element of G -CycleSet holds
( b₄ = CatCycles (c1,c2) iff ex v being Vertex of G st
( v = the Element of (G -VSet (rng c1)) /\ (G -VSet (rng c2)) & b₄ = (Rotate (c1,v)) ^ (Rotate (c2,v)) ) );