let G1 be Supergraph of G; :: thesis: not G1 is edgeless
assume A1: G1 is edgeless ; :: thesis: contradiction
G is Subgraph of G1 by GLIB_006:57;
hence contradiction by A1; :: thesis: verum