let G be _Graph; :: thesis: G is Subgraph of G
for e being set st e in the_Edges_of G holds
( (the_Source_of G) . e = (the_Source_of G) . e & (the_Target_of G) . e = (the_Target_of G) . e ) ;
hence G is Subgraph of G by Def32; :: thesis: verum