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 A1, A2, ZFMISC_1:33;

then card (the_Vertices_of H) = 1 by CARD_1:30;

hence H is _trivial by GLIB_000:def 19; :: thesis: H is Subgraph of G

( 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 A1, A2, ZFMISC_1:33;

then card (the_Vertices_of H) = 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

( (the_Source_of H) . e = (the_Source_of G) . e & (the_Target_of H) . e = (the_Target_of G) . e )

hence
H is Subgraph of G
by A1, GLIB_000:def 32; :: thesis: verum( (the_Source_of H) . e = (the_Source_of G) . e & (the_Target_of H) . e = (the_Target_of G) . e )

let e be set ; :: thesis: ( e in the_Edges_of H implies ( (the_Source_of H) . e = (the_Source_of G) . e & (the_Target_of H) . e = (the_Target_of G) . e ) )

assume A4: e in the_Edges_of H ; :: thesis: ( (the_Source_of H) . e = (the_Source_of G) . e & (the_Target_of H) . e = (the_Target_of G) . e )

then ( (the_Source_of H) . e in the_Vertices_of H & (the_Target_of H) . e in the_Vertices_of H ) by FUNCT_2:5;

then A5: ( (the_Source_of H) . e = v & (the_Target_of H) . e = v ) by A3, TARSKI:def 1;

( (the_Source_of G) . e in the_Vertices_of G & (the_Target_of G) . e in the_Vertices_of G ) by A1, A4, FUNCT_2:5;

hence ( (the_Source_of H) . e = (the_Source_of G) . e & (the_Target_of H) . e = (the_Target_of G) . e ) by A2, A5, TARSKI:def 1; :: thesis: verum

end;assume A4: e in the_Edges_of H ; :: thesis: ( (the_Source_of H) . e = (the_Source_of G) . e & (the_Target_of H) . e = (the_Target_of G) . e )

then ( (the_Source_of H) . e in the_Vertices_of H & (the_Target_of H) . e in the_Vertices_of H ) by FUNCT_2:5;

then A5: ( (the_Source_of H) . e = v & (the_Target_of H) . e = v ) by A3, TARSKI:def 1;

( (the_Source_of G) . e in the_Vertices_of G & (the_Target_of G) . e in the_Vertices_of G ) by A1, A4, FUNCT_2:5;

hence ( (the_Source_of H) . e = (the_Source_of G) . e & (the_Target_of H) . e = (the_Target_of G) . e ) by A2, A5, TARSKI:def 1; :: thesis: verum