let G be _Graph; :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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; :: thesis: for H2 being inducedSubgraph of G,B holds H2 is inducedSubgraph of H1,B

let H2 be inducedSubgraph of G,B; :: thesis: 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;

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;

hence H2 is inducedSubgraph of H1,B by A1, A10, A11, A9, GLIB_000:def 37; :: thesis: verum

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); :: thesis: ( 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 ; :: thesis: 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; :: thesis: for H2 being inducedSubgraph of G,B holds H2 is inducedSubgraph of H1,B

let H2 be inducedSubgraph of G,B; :: thesis: 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 :: thesis: for e being set st e in the_Edges_of H2 holds

e in H1 .edgesBetween B

H1 .edgesBetween B c= the_Edges_of H2
by A2, GLIB_000:76;e in H1 .edgesBetween B

let e be set ; :: thesis: ( e in the_Edges_of H2 implies e in H1 .edgesBetween B )

assume A5: e in the_Edges_of H2 ; :: thesis: e in H1 .edgesBetween B

A6: (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; :: thesis: verum

end;assume A5: e in the_Edges_of H2 ; :: thesis: e in H1 .edgesBetween B

A6: (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; :: thesis: verum

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;

now :: thesis: for e being set st e in the_Edges_of H2 holds

( (the_Source_of H2) . e = (the_Source_of H1) . e & (the_Target_of H2) . e = (the_Target_of H1) . e )

then
H2 is Subgraph of H1
by A1, A10, A11, A3, GLIB_000:def 32;( (the_Source_of H2) . e = (the_Source_of H1) . e & (the_Target_of H2) . e = (the_Target_of H1) . e )

let e be set ; :: thesis: ( e in the_Edges_of H2 implies ( (the_Source_of H2) . e = (the_Source_of H1) . e & (the_Target_of H2) . e = (the_Target_of H1) . e ) )

assume A12: e in the_Edges_of H2 ; :: thesis: ( (the_Source_of H2) . e = (the_Source_of H1) . e & (the_Target_of H2) . e = (the_Target_of H1) . e )

thus (the_Source_of H2) . e = (the_Source_of G) . e by A12, GLIB_000:def 32

.= (the_Source_of H1) . e by A3, A12, GLIB_000:def 32 ; :: thesis: (the_Target_of H2) . e = (the_Target_of H1) . e

thus (the_Target_of H2) . e = (the_Target_of G) . e by A12, GLIB_000:def 32

.= (the_Target_of H1) . e by A3, A12, GLIB_000:def 32 ; :: thesis: verum

end;assume A12: e in the_Edges_of H2 ; :: thesis: ( (the_Source_of H2) . e = (the_Source_of H1) . e & (the_Target_of H2) . e = (the_Target_of H1) . e )

thus (the_Source_of H2) . e = (the_Source_of G) . e by A12, GLIB_000:def 32

.= (the_Source_of H1) . e by A3, A12, GLIB_000:def 32 ; :: thesis: (the_Target_of H2) . e = (the_Target_of H1) . e

thus (the_Target_of H2) . e = (the_Target_of G) . e by A12, GLIB_000:def 32

.= (the_Target_of H1) . e by A3, A12, GLIB_000:def 32 ; :: thesis: verum

hence H2 is inducedSubgraph of H1,B by A1, A10, A11, A9, GLIB_000:def 37; :: thesis: verum