let G2 be _Graph; :: thesis: for G1 being Supergraph of G2
for x being set holds
( ( x in the_Vertices_of G2 implies x in the_Vertices_of G1 ) & ( x in the_Edges_of G2 implies x in the_Edges_of G1 ) )
let G1 be Supergraph of G2; :: thesis: for x being set holds
( ( x in the_Vertices_of G2 implies x in the_Vertices_of G1 ) & ( x in the_Edges_of G2 implies x in the_Edges_of G1 ) )
let x be set ; :: thesis: ( ( x in the_Vertices_of G2 implies x in the_Vertices_of G1 ) & ( x in the_Edges_of G2 implies x in the_Edges_of G1 ) )
G2 is Subgraph of G1 by Th61;
hence ( ( x in the_Vertices_of G2 implies x in the_Vertices_of G1 ) & ( x in the_Edges_of G2 implies x in the_Edges_of G1 ) ) by GLIB_000:42; :: thesis: verum