let V be non empty set ; :: thesis: for E being symmetric Relation of V
for G being GraphFromSymRel of V,E
for X being set holds G .edgesInOut X c= (E | X) \/ (X |` E)
let E be symmetric Relation of V; :: thesis: for G being GraphFromSymRel of V,E
for X being set holds G .edgesInOut X c= (E | X) \/ (X |` E)
let G be GraphFromSymRel of V,E; :: thesis: for X being set holds G .edgesInOut X c= (E | X) \/ (X |` E)
let X be set ; :: thesis: G .edgesInOut X c= (E | X) \/ (X |` E)
(E | X) \/ (X |` E) = (createGraph (V,E)) .edgesInOut X by Th80;
hence G .edgesInOut X c= (E | X) \/ (X |` E) by GLIB_000:76; :: thesis: verum