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 = choose ((G -VSet (rng c1)) /\ (G -VSet (rng c2))) and
A5: CatCycles c1,c2 = (Rotate c1,v) ^ (Rotate c2,v) by A1, A2, Def10;
(G -VSet (rng c1)) /\ (G -VSet (rng c2)) <> {} by A1, XBOOLE_0:def 7;
then A6: ( v in G -VSet (rng c1) & v in G -VSet (rng c2) ) by A4, XBOOLE_0:def 4;

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

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

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

end;

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

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

end;

end;