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
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 )
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;
hence H is Subgraph of G by A1, GLIB_000:def 32; :: thesis: verum