let G be 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 :: thesis: for e being object holds not e in (v .edgesIn()) /\ (v .edgesOut())

given e being object 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 Lm8;
e in v .edgesIn() by A1, XBOOLE_0:def 4;
then (the_Target_of G) . e = v by Lm7;
hence contradiction by A1, A2, Def18; :: 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:35; :: thesis: verum