theorem :: GLIB_000:37

for G being _Graph
for X1, X2, Y1, Y2 being set st X1 c= X2 & Y1 c= Y2 holds
G .edgesBetween (X1,Y1) c= G .edgesBetween (X2,Y2)