let G be _trivial _Graph; :: thesis: for H being _Graph st the_Vertices_of H c= the_Vertices_of G & the_Edges_of H c= the_Edges_of G holds
( H is _trivial & H is Subgraph of G )

let H be _Graph; :: thesis: ( the_Vertices_of H c= the_Vertices_of G & the_Edges_of H c= the_Edges_of G implies ( H is _trivial & H is Subgraph of G ) )
assume A1: ( the_Vertices_of H c= the_Vertices_of G & the_Edges_of H c= the_Edges_of G ) ; :: thesis: ( H is _trivial & H is Subgraph of G )
consider v being Vertex of G such that
A2: the_Vertices_of G = {v} by GLIB_000:22;
A3: the_Vertices_of H = {v} by ;
then card () = 1 by CARD_1:30;
hence H is _trivial by GLIB_000:def 19; :: thesis: H is Subgraph of G
now :: thesis: for e being set st e in the_Edges_of H holds
( () . e = () . e & () . e = () . e )
let e be set ; :: thesis: ( e in the_Edges_of H implies ( () . e = () . e & () . e = () . e ) )
assume A4: e in the_Edges_of H ; :: thesis: ( () . e = () . e & () . e = () . e )
then ( (the_Source_of H) . e in the_Vertices_of H & () . e in the_Vertices_of H ) by FUNCT_2:5;
then A5: ( (the_Source_of H) . e = v & () . e = v ) by ;
( (the_Source_of G) . e in the_Vertices_of G & () . e in the_Vertices_of G ) by ;
hence ( (the_Source_of H) . e = () . e & () . e = () . e ) by ; :: thesis: verum
end;
hence H is Subgraph of G by ; :: thesis: verum