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 Th30
.= Degree (v,(X /\ the carrier' of G)) by Th30 ; :: thesis: verum