let V be non empty set ; :: thesis: for E being Relation of V
for X, Y being set holds (Y |` E) | X = (createGraph (V,E)) .edgesDBetween (X,Y)
let E be Relation of V; :: thesis: for X, Y being set holds (Y |` E) | X = (createGraph (V,E)) .edgesDBetween (X,Y)
let X, Y be set ; :: thesis: (Y |` E) | X = (createGraph (V,E)) .edgesDBetween (X,Y)
thus (Y |` E) | X = (Y |` E) /\ (E | X) by GLIBPRE0:9
.= ((createGraph (V,E)) .edgesInto Y) /\ (E | X) by Th75
.= ((createGraph (V,E)) .edgesInto Y) /\ ((createGraph (V,E)) .edgesOutOf X) by Th74
.= (createGraph (V,E)) .edgesDBetween (X,Y) by GLIB_000:152 ; :: thesis: verum