let G2 be Subgraph of G; :: thesis: G2 is edgeless
the_Edges_of G2 c= the_Edges_of G ;
hence G2 is edgeless ; :: thesis: verum