let V be non empty set ; :: thesis: for E being Relation of V
for X, Y being set holds ((Y |` E) | X) \/ ((X |` E) | Y) = (createGraph (V,E)) .edgesBetween (X,Y)
let E be Relation of V; :: thesis: for X, Y being set holds ((Y |` E) | X) \/ ((X |` E) | Y) = (createGraph (V,E)) .edgesBetween (X,Y)
let X, Y be set ; :: thesis: ((Y |` E) | X) \/ ((X |` E) | Y) = (createGraph (V,E)) .edgesBetween (X,Y)
set G = createGraph (V,E);
thus ((Y |` E) | X) \/ ((X |` E) | Y) = ((Y |` E) | X) \/ ((createGraph (V,E)) .edgesDBetween (Y,X)) by Th76
.= ((createGraph (V,E)) .edgesDBetween (X,Y)) \/ ((createGraph (V,E)) .edgesDBetween (Y,X)) by Th76
.= (createGraph (V,E)) .edgesBetween (X,Y) by GLIBPRE0:28 ; :: thesis: verum