let V be non empty set ; :: thesis: for E being symmetric Relation of V
for G1, G2 being GraphFromSymRel of V,E holds the_Vertices_of G1 = the_Vertices_of G2
let E be symmetric Relation of V; :: thesis: for G1, G2 being GraphFromSymRel of V,E holds the_Vertices_of G1 = the_Vertices_of G2
let G1, G2 be GraphFromSymRel of V,E; :: thesis: the_Vertices_of G1 = the_Vertices_of G2
set G0 = createGraph (V,E);
( the_Vertices_of G1 = the_Vertices_of (createGraph (V,E)) & the_Vertices_of G2 = the_Vertices_of (createGraph (V,E)) ) by GLIB_000:def 33;
hence the_Vertices_of G1 = the_Vertices_of G2 ; :: thesis: verum