let G be _Graph; for A, B being non empty Subset of (the_Vertices_of G) st B c= A holds
for H1 being inducedSubgraph of G,A
for H2 being inducedSubgraph of G,B holds H2 is inducedSubgraph of H1,B
let A, B be non empty Subset of (the_Vertices_of G); ( B c= A implies for H1 being inducedSubgraph of G,A
for H2 being inducedSubgraph of G,B holds H2 is inducedSubgraph of H1,B )
assume A1:
B c= A
; for H1 being inducedSubgraph of G,A
for H2 being inducedSubgraph of G,B holds H2 is inducedSubgraph of H1,B
let H1 be inducedSubgraph of G,A; for H2 being inducedSubgraph of G,B holds H2 is inducedSubgraph of H1,B
let H2 be inducedSubgraph of G,B; H2 is inducedSubgraph of H1,B
A2:
the_Edges_of H2 = G .edgesBetween B
by GLIB_000:def 37;
the_Edges_of H1 = G .edgesBetween A
by GLIB_000:def 37;
then A3:
the_Edges_of H2 c= the_Edges_of H1
by A1, A2, GLIB_000:36;
A4:
now for e being set st e in the_Edges_of H2 holds
e in H1 .edgesBetween Blet e be
set ;
( e in the_Edges_of H2 implies e in H1 .edgesBetween B )assume A5:
e in the_Edges_of H2
;
e in H1 .edgesBetween BA6:
(the_Target_of G) . e = (the_Target_of H1) . e
by A3, A5, GLIB_000:def 32;
A7:
(the_Target_of G) . e in B
by A2, A5, GLIB_000:31;
A8:
(the_Source_of G) . e in B
by A2, A5, GLIB_000:31;
(the_Source_of G) . e = (the_Source_of H1) . e
by A3, A5, GLIB_000:def 32;
hence
e in H1 .edgesBetween B
by A3, A5, A6, A8, A7, GLIB_000:31;
verum end;
H1 .edgesBetween B c= the_Edges_of H2
by A2, GLIB_000:76;
then
for x being object holds
( x in the_Edges_of H2 iff x in H1 .edgesBetween B )
by A4;
then A9:
the_Edges_of H2 = H1 .edgesBetween B
by TARSKI:2;
A10:
the_Vertices_of H1 = A
by GLIB_000:def 37;
A11:
the_Vertices_of H2 = B
by GLIB_000:def 37;
then
H2 is Subgraph of H1
by A1, A10, A11, A3, GLIB_000:def 32;
hence
H2 is inducedSubgraph of H1,B
by A1, A10, A11, A9, GLIB_000:def 37; verum