let G be non void connected finite Graph; :: thesis: for v being Vertex of G holds Degree v <> 0
let v be Vertex of G; :: thesis: Degree v <> 0
assume A1: Degree v = 0 ; :: thesis: contradiction
set E = the carrier' of G;
set T = the Target of G;
set S = the Source of G;
Degree v = Degree v,the carrier' of G by Th29
.= (card (Edges_In v,the carrier' of G)) + (card (Edges_Out v,the carrier' of G)) ;
then ( card (Edges_In v,the carrier' of G) = 0 & card (Edges_Out v,the carrier' of G) = 0 ) by A1;
then A2: ( Edges_In v,the carrier' of G = {} & Edges_Out v,the carrier' of G = {} ) ;
consider e being set such that
A3: e in the carrier' of G by XBOOLE_0:def 1;
reconsider s = the Source of G . e as Vertex of G by A3, FUNCT_2:7;

per cases ( v = s or v <> s ) ;

suppose v = s ; :: thesis: contradiction

hence contradiction by A2, A3, Def2; :: thesis: verum

end;

suppose v <> s ; :: thesis: contradiction

then consider c being Chain of G, vs being FinSequence of the carrier of G such that
A4: ( not c is empty & vs is_vertex_seq_of c & vs . 1 = v & vs . (len vs) = s ) by Th23;
c is FinSequence of the carrier' of G by MSSCYC_1:def 1;
then A5: rng c c= the carrier' of G by FINSEQ_1:def 4;
len c <> 0 by A4;
then 0 < len c ;
then A6: 0 + 1 <= len c by NAT_1:13;
then 1 in dom c by FINSEQ_3:27;
then A7: c . 1 in rng c by FUNCT_1:def 5;
( vs . 1 = the Target of G . (c . 1) or vs . 1 = the Source of G . (c . 1) ) by A4, A6, Lm3;
hence contradiction by A2, A4, A5, A7, Def1, Def2; :: thesis: verum

end;

end;