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