let G be _Graph; :: thesis: for A, B being non empty Subset of () 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 (); :: 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 ;
A4: now :: thesis: for e being set st e in the_Edges_of H2 holds
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 = () . e by ;
A7: (the_Target_of G) . e in B by ;
A8: (the_Source_of G) . e in B by ;
(the_Source_of G) . e = () . e by ;
hence e in H1 .edgesBetween B by ; :: thesis: verum
end;
H1 .edgesBetween B c= the_Edges_of H2 by ;
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
( () . e = () . e & () . e = () . e )
let e be set ; :: thesis: ( e in the_Edges_of H2 implies ( () . e = () . e & () . e = () . e ) )
assume A12: e in the_Edges_of H2 ; :: thesis: ( () . e = () . e & () . e = () . e )
thus () . e = () . e by
.= () . e by ; :: thesis: () . e = () . e
thus () . e = () . e by
.= () . e by ; :: thesis: verum
end;
then H2 is Subgraph of H1 by ;
hence H2 is inducedSubgraph of H1,B by ; :: thesis: verum