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) & 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;
set r1 = Rotate c1,v;
set r2 = Rotate c2,v;
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 (G -CycleSet ) by A5, Th57;
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 (G -CycleSet ) by A5, Th57;
A6: Rotate c1,v = choose Rotated1 by A5, Def9;
A7: Rotate c2,v = choose Rotated2 by A5, Def9;
Rotate c1,v in Rotated1 by A6;
then consider c' being Element of G -CycleSet such that
A8: Rotate c1,v = c' and
A9: rng c' = rng c1 and
A10: ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c' & vs . 1 = v ) ;
Rotate c2,v in Rotated2 by A7;
then consider c'' being Element of G -CycleSet such that
A11: Rotate c2,v = c'' and
A12: rng c'' = rng c2 and
A13: ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c'' & vs . 1 = v ) ;
consider vs1 being FinSequence of the carrier of G such that
A14: ( vs1 is_vertex_seq_of c' & vs1 . 1 = v ) by A10;
consider vs2 being FinSequence of the carrier of G such that
A15: ( vs2 is_vertex_seq_of c'' & vs2 . 1 = v ) by A13;
reconsider c'1 = c' as cyclic Path of G by Def8;
reconsider c'2 = c'' as cyclic Path of G by Def8;
A16: vs2 is_vertex_seq_of c'2 by A15;
vs1 is_vertex_seq_of c'1 by A14;
then A17: vs1 . 1 = vs1 . (len vs1) by MSSCYC_1:6;
A18: ( Rotate c1,v = c'1 & Rotate c2,v = c'2 ) by A8, A11;
then reconsider c = (Rotate c1,v) ^ (Rotate c2,v) as Path of G by A2, A9, A12, A14, A15, A17, Th9;
set vs12 = vs1 ^' vs2;
A19: vs1 ^' vs2 is_vertex_seq_of c by A14, A15, A17, A18, GRAPH_2:47;
len vs1 = (len c') + 1 by A14, GRAPH_2:def 7;
then A20: 1 <= len vs1 by NAT_1:11;
not rng c2 is empty by A5, Th21;
then not c'' is empty by A12;
then len c'' <> 0 ;
then 0 < len c'' ;
then 0 + 1 < (len c'') + 1 by XREAL_1:8;
then A21: 1 < len vs2 by A15, GRAPH_2:def 7;
(vs1 ^' vs2) . 1 = vs1 . 1 by A20, GRAPH_2:14
.= vs2 . (len vs2) by A14, A15, A16, MSSCYC_1:6
.= (vs1 ^' vs2) . (len (vs1 ^' vs2)) by A21, GRAPH_2:16 ;
then c is cyclic by A19, 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