theorem Th26: :: GRAPH_3:26

for e, X being set
for G being finite Graph
for v being Vertex of G st e in the carrier' of G & not e in X & ( v = the Target of G . e or v = the Source of G . e ) holds
Degree v <> Degree (v,X)