let G be Graph; :: thesis: for c1, c2 being Element of G -CycleSet st G -VSet (rng c1) meets G -VSet (rng c2) & rng c1 misses rng c2 & ( c1 <> {} or c2 <> {} ) holds
not CatCycles (c1,c2) is empty
let c1, c2 be Element of G -CycleSet ; :: thesis: ( G -VSet (rng c1) meets G -VSet (rng c2) & rng c1 misses rng c2 & ( c1 <> {} or c2 <> {} ) implies not CatCycles (c1,c2) is empty )
assume that
A1: G -VSet (rng c1) meets G -VSet (rng c2) and
A2: rng c1 misses rng c2 and
A3: ( c1 <> {} or c2 <> {} ) ; :: thesis: not CatCycles (c1,c2) is empty
consider v being Vertex of G such that
A4: v = the Element of (G -VSet (rng c1)) /\ (G -VSet (rng c2)) and
A5: CatCycles (c1,c2) = (Rotate (c1,v)) ^ (Rotate (c2,v)) by A1, A2, Def10;
A6: (G -VSet (rng c1)) /\ (G -VSet (rng c2)) <> {} by A1;
then A7: v in G -VSet (rng c1) by A4, XBOOLE_0:def 4;
A8: v in G -VSet (rng c2) by A4, A6, XBOOLE_0:def 4;

per cases ( c1 <> {} or c2 <> {} ) by A3;

suppose c1 <> {} ; :: thesis: not CatCycles (c1,c2) is empty

then rng (Rotate (c1,v)) <> {} by A7, Lm5;
hence not CatCycles (c1,c2) is empty by A5, FINSEQ_1:35, RELAT_1:38; :: thesis: verum

end;

suppose c2 <> {} ; :: thesis: not CatCycles (c1,c2) is empty

then rng (Rotate (c2,v)) <> {} by A8, Lm5;
hence not CatCycles (c1,c2) is empty by A5, FINSEQ_1:35, RELAT_1:38; :: thesis: verum

end;

end;