A1: the_Vertices_of G1 meets the_Vertices_of G2 by GLIB_012:80;
the_Edges_of G1 misses the_Edges_of G2 by GLIB_012:80;
hence for b₁ being GraphMeet of G1,G2 holds b₁ is edgeless by A1, Th45; :: thesis: verum