let G1 be edgeless _Graph; :: thesis: for G2 being _Graph holds
( G1 is Subgraph of G2 iff the_Vertices_of G1 c= the_Vertices_of G2 )
let G2 be _Graph; :: thesis: ( G1 is Subgraph of G2 iff the_Vertices_of G1 c= the_Vertices_of G2 )
thus ( G1 is Subgraph of G2 implies the_Vertices_of G1 c= the_Vertices_of G2 ) by GLIB_000:def 32; :: thesis: ( the_Vertices_of G1 c= the_Vertices_of G2 implies G1 is Subgraph of G2 )
assume A1: the_Vertices_of G1 c= the_Vertices_of G2 ; :: thesis: G1 is Subgraph of G2
for e being set st e in the_Edges_of G1 holds
( (the_Source_of G1) . e = (the_Source_of G2) . e & (the_Target_of G1) . e = (the_Target_of G2) . e ) ;
hence G1 is Subgraph of G2 by A1, XBOOLE_1:2, GLIB_000:def 32; :: thesis: verum