let X be set ; :: thesis: for G being finite Graph
for v being Vertex of G holds Degree v,X = Degree v,(X /\ the carrier' of G)
let G be finite Graph; :: thesis: for v being Vertex of G holds Degree v,X = Degree v,(X /\ the carrier' of G)
let v be Vertex of G; :: thesis: Degree v,X = Degree v,(X /\ the carrier' of G)
set E = the carrier' of G;
thus Degree v,X = (card (Edges_In v,(X /\ the carrier' of G))) + (card (Edges_Out v,X)) by Th35
.= Degree v,(X /\ the carrier' of G) by Th35 ; :: thesis: verum