for V being non empty set
for E being symmetric Relation of V
for G1, G2 being GraphFromSymRel of V,E holds the_Vertices_of G1 = the_Vertices_of G2