let G be simple _Graph; for v being Vertex of G holds v .degree() = card (v .allNeighbors())
let v be Vertex of G; v .degree() = card (v .allNeighbors())
(v .inNeighbors()) /\ (v .outNeighbors()) = {}
proof
assume
(v .inNeighbors()) /\ (v .outNeighbors()) <> {}
;
contradiction
then consider w being
object such that A1:
w in (v .inNeighbors()) /\ (v .outNeighbors())
by XBOOLE_0:def 1;
A2:
(
w in v .inNeighbors() &
w in v .outNeighbors() )
by A1, XBOOLE_0:def 4;
consider e1 being
object such that A3:
e1 DJoins w,
v,
G
by A2, GLIB_000:69;
consider e2 being
object such that A4:
e2 DJoins v,
w,
G
by A2, GLIB_000:70;
(
e1 Joins v,
w,
G &
e2 Joins v,
w,
G )
by A3, A4, GLIB_000:16;
then
e1 = e2
by GLIB_000:def 20;
then
(
e1 in the_Edges_of G &
(the_Source_of G) . e1 = v &
(the_Target_of G) . e1 = v )
by A3, A4, GLIB_000:def 14;
hence
contradiction
by GLIB_000:def 18;
verum
end;
then card ((v .inNeighbors()) \/ (v .outNeighbors())) =
(card (v .inNeighbors())) +` (card (v .outNeighbors()))
by CARD_2:35, XBOOLE_0:def 7
.=
(v .inDegree()) +` (card (v .outNeighbors()))
by Th3
.=
(v .inDegree()) +` (v .outDegree())
by Th4
.=
v .degree()
by GLIB_000:def 44
;
hence
v .degree() = card (v .allNeighbors())
by GLIB_000:def 48; verum