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 Th27
.= (card (Edges_In v,the carrier' of G)) + (card (Edges_Out v)) by Th28
.= Degree v,the carrier' of G ; :: thesis: verum