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;

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 ) )

hence
G2 .edgesBetween T = G .edgesBetween T
by TARSKI:2; :: thesis: verum( ( 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 ) )

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;hereby :: thesis: ( e in G2 .edgesBetween T implies e in G .edgesBetween T )

assume A8:
e in G2 .edgesBetween T
; :: thesis: e in G .edgesBetween Tassume 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;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

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