set X = { v' where v' is Vertex of G : ( v' in G -VSet (rng c) & Degree v' <> Degree v',(rng c) ) } ;
set v = choose { v' where v' is Vertex of G : ( v' in G -VSet (rng c) & Degree v' <> Degree v',(rng c) ) } ;
not { v' where v' is Vertex of G : ( v' in G -VSet (rng c) & Degree v' <> Degree v',(rng c) ) } is empty by A1, A2, Th61;
then choose { v' where v' is Vertex of G : ( v' in G -VSet (rng c) & Degree v' <> Degree v',(rng c) ) } in { v' where v' is Vertex of G : ( v' in G -VSet (rng c) & Degree v' <> Degree v',(rng c) ) } ;
then ex v' being Vertex of G st
( choose { v' where v' is Vertex of G : ( v' in G -VSet (rng c) & Degree v' <> Degree v',(rng c) ) } = v' & v' in G -VSet (rng c) & Degree v' <> Degree v',(rng c) ) ;
then reconsider v = choose { v' where v' is Vertex of G : ( v' in G -VSet (rng c) & Degree v' <> Degree v',(rng c) ) } as Vertex of G ;
set E = the carrier' of G;
reconsider E' = 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 = E' \ (rng c) as non empty finite set by XBOOLE_0:def 5;
set c' = choose (Erc -CycleSet v);
choose (Erc -CycleSet v) in Erc -CycleSet v ;
then reconsider c' = choose (Erc -CycleSet v) as Element of G -CycleSet ;
reconsider IT = CatCycles c,c' as Element of G -CycleSet ;
take IT ; :: thesis: ex c' being Element of G -CycleSet ex v being Vertex of G st
( v = choose { v' where v' is Vertex of G : ( v' in G -VSet (rng c) & Degree v' <> Degree v',(rng c) ) } & c' = choose ((the carrier' of G \ (rng c)) -CycleSet v) & IT = CatCycles c,c' )
take c' ; :: thesis: ex v being Vertex of G st
( v = choose { v' where v' is Vertex of G : ( v' in G -VSet (rng c) & Degree v' <> Degree v',(rng c) ) } & c' = choose ((the carrier' of G \ (rng c)) -CycleSet v) & IT = CatCycles c,c' )
take v ; :: thesis: ( v = choose { v' where v' is Vertex of G : ( v' in G -VSet (rng c) & Degree v' <> Degree v',(rng c) ) } & c' = choose ((the carrier' of G \ (rng c)) -CycleSet v) & IT = CatCycles c,c' )
thus ( v = choose { v' where v' is Vertex of G : ( v' in G -VSet (rng c) & Degree v' <> Degree v',(rng c) ) } & c' = choose ((the carrier' of G \ (rng c)) -CycleSet v) & IT = CatCycles c,c' ) ; :: thesis: verum