let G be _Graph; for S, T being non empty Subset of st T c= S holds
for G2 being inducedSubgraph of ,G holds G2 .edgesBetween T = G .edgesBetween T
let S, T be non empty Subset of ; ( T c= S implies for G2 being inducedSubgraph of ,G holds G2 .edgesBetween T = G .edgesBetween T )
assume A1:
T c= S
; for G2 being inducedSubgraph of ,G holds G2 .edgesBetween T = G .edgesBetween T
let G2 be inducedSubgraph of ,G; G2 .edgesBetween T = G .edgesBetween T
A2:
the_Edges_of G2 = G .edgesBetween S
by GLIB_000:def 39;
now let e be
set ;
( ( e in G .edgesBetween T implies e in G2 .edgesBetween T ) & ( e in G2 .edgesBetween T implies e in G .edgesBetween T ) )hereby ( e in G2 .edgesBetween T implies e in G .edgesBetween T )
assume A3:
e in G .edgesBetween T
;
e in G2 .edgesBetween Tthen A4:
(the_Source_of G) . e in T
by GLIB_000:34;
A5:
(the_Target_of G) . e in T
by A3, GLIB_000:34;
A6:
G .edgesBetween T c= G .edgesBetween S
by A1, GLIB_000:39;
then A7:
(the_Target_of G2) . e = (the_Target_of G) . e
by A2, A3, GLIB_000:def 34;
(the_Source_of G2) . e = (the_Source_of G) . e
by A2, A3, A6, GLIB_000:def 34;
hence
e in G2 .edgesBetween T
by A2, A3, A6, A4, A5, A7, GLIB_000:34;
verum
end; assume A8:
e in G2 .edgesBetween T
;
e in G .edgesBetween Tthen
(the_Source_of G2) . e in T
by GLIB_000:34;
then A9:
(the_Source_of G) . e in T
by A8, GLIB_000:def 34;
(the_Target_of G2) . e in T
by A8, GLIB_000:34;
then A10:
(the_Target_of G) . e in T
by A8, GLIB_000:def 34;
e in the_Edges_of G2
by A8;
hence
e in G .edgesBetween T
by A9, A10, GLIB_000:34;
verum end;
hence
G2 .edgesBetween T = G .edgesBetween T
by TARSKI:2; verum