set Rotated = { c' where c' is Element of G -CycleSet : ( rng c' = rng c & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c' & vs . 1 = v ) ) } ;
set IT = choose { c' where c' is Element of G -CycleSet : ( rng c' = rng c & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c' & vs . 1 = v ) ) } ;
not { c' where c' is Element of G -CycleSet : ( rng c' = rng c & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c' & vs . 1 = v ) ) } is empty by A1, Th57;
then choose { c' where c' is Element of G -CycleSet : ( rng c' = rng c & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c' & vs . 1 = v ) ) } in { c' where c' is Element of G -CycleSet : ( rng c' = rng c & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c' & vs . 1 = v ) ) } ;
then consider c' being Element of G -CycleSet such that
A2: ( choose { c' where c' is Element of G -CycleSet : ( rng c' = rng c & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c' & vs . 1 = v ) ) } = c' & rng c' = rng c & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c' & vs . 1 = v ) ) ;
thus choose { c' where c' is Element of G -CycleSet : ( rng c' = rng c & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c' & vs . 1 = v ) ) } is Element of G -CycleSet by A2; :: thesis: verum