consider v1, v2 being Vertex of G such that
A1: v1 <> v2 by GLIB_000:21;
reconsider v1 = v1, v2 = v2 as Vertex of G2 by GLIB_000:53;
take v1 ; :: thesis:
take v2 ; :: thesis:
thus v1 <> v2 by A1; :: thesis:

end;