set X = { v9 where v9 is Vertex of G : ( v9 in G -VSet (rng c) & Degree v9 <> Degree (v9,(rng c)) ) } ;
set v = choose { v9 where v9 is Vertex of G : ( v9 in G -VSet (rng c) & Degree v9 <> Degree (v9,(rng c)) ) } ;
not { v9 where v9 is Vertex of G : ( v9 in G -VSet (rng c) & Degree v9 <> Degree (v9,(rng c)) ) } is empty by A1, A2, Th61;
then choose { v9 where v9 is Vertex of G : ( v9 in G -VSet (rng c) & Degree v9 <> Degree (v9,(rng c)) ) } in { v9 where v9 is Vertex of G : ( v9 in G -VSet (rng c) & Degree v9 <> Degree (v9,(rng c)) ) } ;
then ex v9 being Vertex of G st
( choose { v9 where v9 is Vertex of G : ( v9 in G -VSet (rng c) & Degree v9 <> Degree (v9,(rng c)) ) } = v9 & v9 in G -VSet (rng c) & Degree v9 <> Degree (v9,(rng c)) ) ;
then reconsider v = choose { v9 where v9 is Vertex of G : ( v9 in G -VSet (rng c) & Degree v9 <> Degree (v9,(rng c)) ) } as Vertex of G ;
set E = the carrier' of G;
reconsider E9 = the carrier' of G as finite set by GRAPH_1:def 9;
rng c c= the carrier' of G by FINSEQ_1:def 4;
then rng c c< the carrier' of G by A1, XBOOLE_0:def 8;
then ex xx being set st
( xx in the carrier' of G & not xx in rng c ) by XBOOLE_0:6;
then reconsider Erc = E9 \ (rng c) as non empty finite set by XBOOLE_0:def 5;
set c9 = choose (Erc -CycleSet v);
choose (Erc -CycleSet v) in Erc -CycleSet v ;
then reconsider c9 = choose (Erc -CycleSet v) as Element of G -CycleSet ;
reconsider IT = CatCycles (c,c9) as Element of G -CycleSet ;
take IT ; :: thesis: ex c9 being Element of G -CycleSet ex v being Vertex of G st
( v = choose { v9 where v9 is Vertex of G : ( v9 in G -VSet (rng c) & Degree v9 <> Degree (v9,(rng c)) ) } & c9 = choose (( the carrier' of G \ (rng c)) -CycleSet v) & IT = CatCycles (c,c9) )
take c9 ; :: thesis: ex v being Vertex of G st
( v = choose { v9 where v9 is Vertex of G : ( v9 in G -VSet (rng c) & Degree v9 <> Degree (v9,(rng c)) ) } & c9 = choose (( the carrier' of G \ (rng c)) -CycleSet v) & IT = CatCycles (c,c9) )
take v ; :: thesis: ( v = choose { v9 where v9 is Vertex of G : ( v9 in G -VSet (rng c) & Degree v9 <> Degree (v9,(rng c)) ) } & c9 = choose (( the carrier' of G \ (rng c)) -CycleSet v) & IT = CatCycles (c,c9) )
thus ( v = choose { v9 where v9 is Vertex of G : ( v9 in G -VSet (rng c) & Degree v9 <> Degree (v9,(rng c)) ) } & c9 = choose (( the carrier' of G \ (rng c)) -CycleSet v) & IT = CatCycles (c,c9) ) ; :: thesis: verum