let G be _Graph; :: thesis: for v being Vertex of G st ( for e being object holds not e Joins v,v,G ) holds
card (v .edgesInOut()) = v .degree()
let v be Vertex of G; :: thesis: ( ( for e being object holds not e Joins v,v,G ) implies card (v .edgesInOut()) = v .degree() )
assume A1: for e being object holds not e Joins v,v,G ; :: thesis: card (v .edgesInOut()) = v .degree()
(v .edgesIn()) /\ (v .edgesOut()) = {}
proof
assume (v .edgesIn()) /\ (v .edgesOut()) <> {} ; :: thesis: contradiction
then consider e being object such that
A2: e in (v .edgesIn()) /\ (v .edgesOut()) by XBOOLE_0:def 1;
( e in v .edgesIn() & e in v .edgesOut() ) by A2, XBOOLE_0:def 4;
then ( e in the_Edges_of G & (the_Target_of G) . e = v & (the_Source_of G) . e = v ) by GLIB_000:56, GLIB_000:58;
then e Joins v,v,G by GLIB_000:def 13;
hence contradiction by A1; :: thesis: verum
end;
hence card (v .edgesInOut()) = v .degree() by CARD_2:35, XBOOLE_0:def 7; :: thesis: verum