let G be finite Graph; :: thesis: for v being Vertex of G holds Degree v = Degree (v, the carrier' of G)
let v be Vertex of G; :: thesis: Degree v = Degree (v, the carrier' of G)
thus Degree v = (card (Edges_In v)) + (EdgesOut v) by Th22
.= (card (Edges_In (v, the carrier' of G))) + (card (Edges_Out v)) by Th23
.= Degree (v, the carrier' of G) ; :: thesis: verum