let G be finite Graph; :: thesis: for v being Vertex of G holds card (Edges_In v) = EdgesIn v
let v be Vertex of G; :: thesis: card (Edges_In v) = EdgesIn v
consider X being finite set such that
A1: for z being set holds
( z in X iff ( z in the carrier' of G & the Target of G . z = v ) ) and
A2: EdgesIn v = card X by GRAPH_1:def 21;

now :: thesis: for e being object holds
( e in Edges_In v iff e in X )

let e be object ; :: thesis: ( e in Edges_In v iff e in X )
( e in Edges_In (v, the carrier' of G) iff ( e in the carrier' of G & the Target of G . e = v ) ) by Def1;
hence ( e in Edges_In v iff e in X ) by A1; :: thesis: verum

end;

hence card (Edges_In v) = EdgesIn v by A2, TARSKI:2; :: thesis: verum