set X = { v9 where v9 is Vertex of G : ( v9 in G -VSet (rng c) & Degree v9 <> Degree (v9,(rng c)) ) } ;
set v = the Element of { 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, Th56;
then the Element of { 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
( the Element of { 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 = the Element of { 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 11;
rng c c= the carrier' of G by FINSEQ_1:def 4;
then rng c c< the carrier' of G by A1;
then ex xx being object 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 = the Element of Erc -CycleSet v;
the Element of Erc -CycleSet v in Erc -CycleSet v ;
then reconsider c9 = the Element of 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 = the Element of { v9 where v9 is Vertex of G : ( v9 in G -VSet (rng c) & Degree v9 <> Degree (v9,(rng c)) ) } & c9 = the Element of ( the carrier' of G \ (rng c)) -CycleSet v & IT = CatCycles (c,c9) )
take c9 ; :: thesis: ex v being Vertex of G st
( v = the Element of { v9 where v9 is Vertex of G : ( v9 in G -VSet (rng c) & Degree v9 <> Degree (v9,(rng c)) ) } & c9 = the Element of ( the carrier' of G \ (rng c)) -CycleSet v & IT = CatCycles (c,c9) )
take v ; :: thesis: ( v = the Element of { v9 where v9 is Vertex of G : ( v9 in G -VSet (rng c) & Degree v9 <> Degree (v9,(rng c)) ) } & c9 = the Element of ( the carrier' of G \ (rng c)) -CycleSet v & IT = CatCycles (c,c9) )
thus ( v = the Element of { v9 where v9 is Vertex of G : ( v9 in G -VSet (rng c) & Degree v9 <> Degree (v9,(rng c)) ) } & c9 = the Element of ( the carrier' of G \ (rng c)) -CycleSet v & IT = CatCycles (c,c9) ) ; :: thesis: verum