let G be simple _Graph; :: thesis: for v being Vertex of G holds v .degree() = card (v .allNeighbors())
let v be Vertex of G; :: thesis: v .degree() = card (v .allNeighbors())
(v .inNeighbors()) /\ (v .outNeighbors()) = {}

proof

assume (v .inNeighbors()) /\ (v .outNeighbors()) <> {} ; :: thesis: 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, Th69;
consider e2 being object such that
A4: e2 DJoins v,w,G by A2, Th70;
( e1 Joins v,w,G & e2 Joins v,w,G ) by A3, A4;
then e1 = e2 by Def20;
then ( e1 in the_Edges_of G & (the_Source_of G) . e1 = v & (the_Target_of G) . e1 = v ) by A3, A4;
hence contradiction by Def18; :: thesis: 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 Th109
.= v .degree() by Th110 ;
hence v .degree() = card (v .allNeighbors()) ; :: thesis: verum