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
; 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
; 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
; ( 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) )
; verum