let G be finite loopless _Graph; :: thesis: for v being Vertex of G holds v .degree() = card (v .edgesInOut() )
let v be Vertex of G; :: thesis: v .degree() = card (v .edgesInOut() )
set In = v .edgesIn() ;
set Out = v .edgesOut() ;

now

given e being set such that A1: e in (v .edgesIn() ) /\ (v .edgesOut() ) ; :: thesis: contradiction
e in v .edgesOut() by A1, XBOOLE_0:def 4;
then A2: (the_Source_of G) . e = v by Lm9;
e in v .edgesIn() by A1, XBOOLE_0:def 4;
then (the_Target_of G) . e = v by Lm8;
hence contradiction by A1, A2, Def20; :: thesis: verum

end;

then (v .edgesIn() ) /\ (v .edgesOut() ) = {} by XBOOLE_0:def 1;
then v .edgesIn() misses v .edgesOut() by XBOOLE_0:def 7;
hence v .degree() = card (v .edgesInOut() ) by CARD_2:53; :: thesis: verum