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 .edgesIn() & e in v .edgesOut() ) by A1, XBOOLE_0:def 4;
then ( e in the_Edges_of G & (the_Source_of G) . e = v & (the_Target_of G) . e = v ) by Lm8, Lm9;
hence contradiction by 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