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 H1,B holds H2 is inducedSubgraph of G,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 H1,B holds H2 is inducedSubgraph of G,B )
assume A1: B c= A ; :: thesis: for H1 being inducedSubgraph of G,A
for H2 being inducedSubgraph of H1,B holds H2 is inducedSubgraph of G,B
let H1 be inducedSubgraph of G,A; :: thesis: for H2 being inducedSubgraph of H1,B holds H2 is inducedSubgraph of G,B
let H2 be inducedSubgraph of H1,B; :: thesis: H2 is inducedSubgraph of G,B
A2: the_Vertices_of H1 = A by GLIB_000:def 39;
then A3: the_Vertices_of H2 = B by A1, GLIB_000:def 39;
( the_Edges_of H2 c= the_Edges_of H1 & the_Edges_of H1 c= the_Edges_of G ) ;
then A4: the_Edges_of H2 c= the_Edges_of G by XBOOLE_1:1;

now

let e be set ; :: thesis: ( e in the_Edges_of H2 implies ( (the_Source_of H2) . e = (the_Source_of G) . e & (the_Target_of H2) . e = (the_Target_of G) . e ) )
assume A5: e in the_Edges_of H2 ; :: thesis: ( (the_Source_of H2) . e = (the_Source_of G) . e & (the_Target_of H2) . e = (the_Target_of G) . e )
( (the_Source_of H2) . e = (the_Source_of H1) . e & (the_Target_of H2) . e = (the_Target_of H1) . e ) by A5, GLIB_000:def 34;
hence ( (the_Source_of H2) . e = (the_Source_of G) . e & (the_Target_of H2) . e = (the_Target_of G) . e ) by A5, GLIB_000:def 34; :: thesis: verum

end;

then A6: H2 is Subgraph of G by A3, A4, GLIB_000:def 34;
H1 .edgesBetween B c= G .edgesBetween B by GLIB_000:79;
then A7: the_Edges_of H2 c= G .edgesBetween B by A1, A2, GLIB_000:def 39;

now

let e be set ; :: thesis: ( e in G .edgesBetween B implies e in the_Edges_of H2 )
assume A8: e in G .edgesBetween B ; :: thesis: e in the_Edges_of H2
A9: ( (the_Source_of G) . e in B & (the_Target_of G) . e in B ) by A8, GLIB_000:34;
then e in G .edgesBetween A by A1, A8, GLIB_000:34;
then A10: e in the_Edges_of H1 by GLIB_000:def 39;
then ( (the_Source_of H1) . e = (the_Source_of G) . e & (the_Target_of H1) . e = (the_Target_of G) . e ) by GLIB_000:def 34;
then e in H1 .edgesBetween B by A9, A10, GLIB_000:34;
hence e in the_Edges_of H2 by A1, A2, GLIB_000:def 39; :: thesis: verum

end;

then for x being set holds
( x in the_Edges_of H2 iff x in G .edgesBetween B ) by A7;
then the_Edges_of H2 = G .edgesBetween B by TARSKI:2;
hence H2 is inducedSubgraph of G,B by A3, A6, GLIB_000:def 39; :: thesis: verum