let G be _Graph; :: thesis: for S, T being non empty Subset of (the_Vertices_of G) st T c= S holds
for G2 being inducedSubgraph of G,S holds G2 .edgesBetween T = G .edgesBetween T
let S, T be non empty Subset of (the_Vertices_of G); :: thesis: ( T c= S implies for G2 being inducedSubgraph of G,S holds G2 .edgesBetween T = G .edgesBetween T )
assume A1: T c= S ; :: thesis: for G2 being inducedSubgraph of G,S holds G2 .edgesBetween T = G .edgesBetween T
let G2 be inducedSubgraph of G,S; :: thesis: G2 .edgesBetween T = G .edgesBetween T
A2: the_Edges_of G2 = G .edgesBetween S by GLIB_000:def 37;

now :: thesis: for e being object holds
( ( e in G .edgesBetween T implies e in G2 .edgesBetween T ) & ( e in G2 .edgesBetween T implies e in G .edgesBetween T ) )

let e be object ; :: thesis: ( ( e in G .edgesBetween T implies e in G2 .edgesBetween T ) & ( e in G2 .edgesBetween T implies e in G .edgesBetween T ) )

hereby :: thesis: ( e in G2 .edgesBetween T implies e in G .edgesBetween T )

assume A3: e in G .edgesBetween T ; :: thesis: e in G2 .edgesBetween T
then A4: (the_Source_of G) . e in T by GLIB_000:31;
A5: (the_Target_of G) . e in T by A3, GLIB_000:31;
A6: G .edgesBetween T c= G .edgesBetween S by A1, GLIB_000:36;
then A7: (the_Target_of G2) . e = (the_Target_of G) . e by A2, A3, GLIB_000:def 32;
(the_Source_of G2) . e = (the_Source_of G) . e by A2, A3, A6, GLIB_000:def 32;
hence e in G2 .edgesBetween T by A2, A3, A6, A4, A5, A7, GLIB_000:31; :: thesis: verum

end;

assume A8: e in G2 .edgesBetween T ; :: thesis: e in G .edgesBetween T
then (the_Source_of G2) . e in T by GLIB_000:31;
then A9: (the_Source_of G) . e in T by A8, GLIB_000:def 32;
(the_Target_of G2) . e in T by A8, GLIB_000:31;
then A10: (the_Target_of G) . e in T by A8, GLIB_000:def 32;
e in the_Edges_of G2 by A8;
hence e in G .edgesBetween T by A9, A10, GLIB_000:31; :: thesis: verum

end;

hence G2 .edgesBetween T = G .edgesBetween T by TARSKI:2; :: thesis: verum