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