theorem :: GLIB_000:32

for G being _Graph
for X being set
for e, x, y being object st x in X & y in X & e Joins x,y,G holds
e in G .edgesBetween X by Lm5;