set v = choose ((G -VSet (rng c1)) /\ (G -VSet (rng c2)));
A3: not (G -VSet (rng c1)) /\ (G -VSet (rng c2)) is empty by A1, XBOOLE_0:def 7;
then A4: choose ((G -VSet (rng c1)) /\ (G -VSet (rng c2))) in (G -VSet (rng c1)) /\ (G -VSet (rng c2)) ;
A5: choose ((G -VSet (rng c1)) /\ (G -VSet (rng c2))) in G -VSet (rng c1) by A3, XBOOLE_0:def 4;
A6: choose ((G -VSet (rng c1)) /\ (G -VSet (rng c2))) in G -VSet (rng c2) by A3, XBOOLE_0:def 4;
reconsider v = choose ((G -VSet (rng c1)) /\ (G -VSet (rng c2))) as Vertex of G by A4;
reconsider Rotated2 = { c' where c' is Element of G -CycleSet : ( rng c' = rng c2 & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c' & vs . 1 = v ) ) } as non empty Subset of by A6, Th57;
set r2 = Rotate c2,v;
Rotate c2,v = choose Rotated2 by A6, Def9;
then Rotate c2,v in Rotated2 ;
then consider c'' being Element of G -CycleSet such that
A7: Rotate c2,v = c'' and
A8: rng c'' = rng c2 and
A9: ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c'' & vs . 1 = v ) ;
consider vs2 being FinSequence of the carrier of G such that
A10: vs2 is_vertex_seq_of c'' and
A11: vs2 . 1 = v by A9;
reconsider c'2 = c'' as cyclic Path of cyclic by Def8;
A12: Rotate c2,v = c'2 by A7;
not rng c2 is empty by A6, Th21;
then not c'' is empty by A8;
then 0 + 1 < (len c'') + 1 by XREAL_1:8;
then A13: 1 < len vs2 by A10, GRAPH_2:def 7;
A14: vs2 is_vertex_seq_of c'2 by A10;
reconsider Rotated1 = { c' where c' is Element of G -CycleSet : ( rng c' = rng c1 & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c' & vs . 1 = v ) ) } as non empty Subset of by A5, Th57;
set r1 = Rotate c1,v;
Rotate c1,v = choose Rotated1 by A5, Def9;
then Rotate c1,v in Rotated1 ;
then consider c' being Element of G -CycleSet such that
A15: Rotate c1,v = c' and
A16: rng c' = rng c1 and
A17: ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c' & vs . 1 = v ) ;
reconsider c'1 = c' as cyclic Path of cyclic by Def8;
consider vs1 being FinSequence of the carrier of G such that
A18: vs1 is_vertex_seq_of c' and
A19: vs1 . 1 = v by A17;
vs1 is_vertex_seq_of c'1 by A18;
then A20: vs1 . 1 = vs1 . (len vs1) by MSSCYC_1:6;
set vs12 = vs1 ^' vs2;
len vs1 = (len c') + 1 by A18, GRAPH_2:def 7;
then 1 <= len vs1 by NAT_1:11;
then A21: (vs1 ^' vs2) . 1 = vs1 . 1 by GRAPH_2:14
.= vs2 . (len vs2) by A19, A11, A14, MSSCYC_1:6
.= (vs1 ^' vs2) . (len (vs1 ^' vs2)) by A13, GRAPH_2:16 ;
A22: Rotate c1,v = c'1 by A15;
then reconsider c = (Rotate c1,v) ^ (Rotate c2,v) as Path of by A2, A16, A8, A18, A19, A10, A11, A20, A12, Th9;
vs1 ^' vs2 is_vertex_seq_of c by A18, A19, A10, A11, A20, A22, A12, GRAPH_2:47;
then c is cyclic by A21, MSSCYC_1:def 2;
then reconsider c = c as Element of G -CycleSet by Def8;
take c ; :: thesis: ex v being Vertex of G st
( v = choose ((G -VSet (rng c1)) /\ (G -VSet (rng c2))) & c = (Rotate c1,v) ^ (Rotate c2,v) )
take v ; :: thesis: ( v = choose ((G -VSet (rng c1)) /\ (G -VSet (rng c2))) & c = (Rotate c1,v) ^ (Rotate c2,v) )
thus ( v = choose ((G -VSet (rng c1)) /\ (G -VSet (rng c2))) & c = (Rotate c1,v) ^ (Rotate c2,v) ) ; :: thesis: verum