let G1 be connected _Graph; :: thesis: for G2 being Subgraph of G1 st the_Edges_of G1 c= the_Edges_of G2 holds
G1 == G2
let G2 be Subgraph of G1; :: thesis: ( the_Edges_of G1 c= the_Edges_of G2 implies G1 == G2 )
assume A1: the_Edges_of G1 c= the_Edges_of G2 ; :: thesis: G1 == G2
A2: the_Edges_of G1 = the_Edges_of G2 by A1, XBOOLE_0:def 10;
A3: G1 is Subgraph of G1 by GLIB_000:40;
the_Vertices_of G1 = the_Vertices_of G2

proof

per cases ( not G1 is _trivial or G1 is _trivial ) ;

suppose A4: not G1 is _trivial ; :: thesis: the_Vertices_of G1 = the_Vertices_of G2

assume the_Vertices_of G1 <> the_Vertices_of G2 ; :: thesis: contradiction
then not the_Vertices_of G1 c= the_Vertices_of G2 by XBOOLE_0:def 10;
then A5: (the_Vertices_of G1) \ (the_Vertices_of G2) <> {} by XBOOLE_1:37;
set v = the Element of (the_Vertices_of G1) \ (the_Vertices_of G2);
reconsider v = the Element of (the_Vertices_of G1) \ (the_Vertices_of G2) as Vertex of G1 by A5, TARSKI:def 3;

per cases ( v .edgesInOut() = {} or v .edgesInOut() <> {} ) ;

suppose v .edgesInOut() = {} ; :: thesis: contradiction

hence contradiction by A4, GLIB_000:def 49; :: thesis: verum

end;

suppose A6: v .edgesInOut() <> {} ; :: thesis: contradiction

set e = the Element of v .edgesInOut() ;

per cases ( (the_Source_of G1) . the Element of v .edgesInOut() = v or (the_Target_of G1) . the Element of v .edgesInOut() = v ) by A6, GLIB_000:61;

suppose A7: (the_Source_of G1) . the Element of v .edgesInOut() = v ; :: thesis: contradiction

A8: the Element of v .edgesInOut() in the_Edges_of G2 by A2, A6, GLIB_000:61;
then (the_Source_of G2) . the Element of v .edgesInOut() = v by A7, GLIB_000:def 32;
then v in the_Vertices_of G2 by A8, FUNCT_2:5;
hence contradiction by A5, XBOOLE_0:def 5; :: thesis: verum

end;

suppose A9: (the_Target_of G1) . the Element of v .edgesInOut() = v ; :: thesis: contradiction

A10: the Element of v .edgesInOut() in the_Edges_of G2 by A2, A6, GLIB_000:61;
then (the_Target_of G2) . the Element of v .edgesInOut() = v by A9, GLIB_000:def 32;
then v in the_Vertices_of G2 by A10, FUNCT_2:5;
hence contradiction by A5, XBOOLE_0:def 5; :: thesis: verum

end;

end;

end;

end;

end;

suppose A11: G1 is _trivial ; :: thesis: the_Vertices_of G1 = the_Vertices_of G2

then consider v1 being Vertex of G1 such that
A12: the_Vertices_of G1 = {v1} by GLIB_000:22;
consider v2 being Vertex of G2 such that
A13: the_Vertices_of G2 = {v2} by A11, GLIB_000:22;
thus the_Vertices_of G1 = the_Vertices_of G2 by A12, A13, ZFMISC_1:3; :: thesis: verum

end;

end;

end;

hence G1 == G2 by A2, A3, GLIB_000:86; :: thesis: verum