let G be non void connected finite Graph; for v being Vertex of G holds Degree v <> 0
let v be Vertex of G; Degree v <> 0
assume A1:
Degree v = 0
; contradiction
set E = the carrier' of G;
A2: Degree v =
Degree (v, the carrier' of G)
by Th24
.=
(card (Edges_In (v, the carrier' of G))) + (card (Edges_Out (v, the carrier' of G)))
;
then A3:
Edges_In (v, the carrier' of G) = {}
by A1;
A4:
Edges_Out (v, the carrier' of G) = {}
by A1, A2;
set S = the Source of G;
set T = the Target of G;
consider e being object such that
A5:
e in the carrier' of G
by XBOOLE_0:def 1;
reconsider s = the Source of G . e as Vertex of G by A5, FUNCT_2:5;
per cases
( v = s or v <> s )
;
suppose
v <> s
;
contradictionthen consider c being
Chain of
G,
vs being
FinSequence of the
carrier of
G such that A6:
not
c is
empty
and A7:
vs is_vertex_seq_of c
and A8:
vs . 1
= v
and
vs . (len vs) = s
by Th18;
A9:
0 + 1
<= len c
by A6, NAT_1:13;
then
1
in dom c
by FINSEQ_3:25;
then A10:
c . 1
in rng c
by FUNCT_1:def 3;
c is
FinSequence of the
carrier' of
G
by MSSCYC_1:def 1;
then A11:
rng c c= the
carrier' of
G
by FINSEQ_1:def 4;
(
vs . 1
= the
Target of
G . (c . 1) or
vs . 1
= the
Source of
G . (c . 1) )
by A7, A9, Lm3;
hence
contradiction
by A3, A4, A8, A11, A10, Def1, Def2;
verum end;