set V = the_Vertices_of G;
deffunc H₁( object ) -> plain inducedSubgraph of G,(Segm G) = the plain inducedSubgraph of G,(Segm G);
consider f being Function such that
A1: dom f = bool (the_Vertices_of G) and
A2: for x being object st x in bool (the_Vertices_of G) holds
f . x = H₁(x) from FUNCT_1:sch 3();
A3: rng f is finite by A1, FINSET_1:8;

now :: thesis: for h being object st h in G .allInducedSG() holds
h in rng f

let h be object ; :: thesis: ( h in G .allInducedSG() implies h in rng f )
assume A4: h in G .allInducedSG() ; :: thesis: h in rng f
then reconsider H = h as _Graph ;
consider W being non empty Subset of (the_Vertices_of G) such that
A5: H is plain inducedSubgraph of G,W by A4, Th45;
A6: Segm W = W by ORDINAL1:def 17;
f . W = the plain inducedSubgraph of G,W by A2, A6;
then H = f . W by A5, GLIB_000:93, GLIB_009:44;
hence h in rng f by A1, FUNCT_1:def 3; :: thesis: verum

end;

then G .allInducedSG() c= rng f by TARSKI:def 3;
hence G .allInducedSG() is finite by A3; :: thesis: verum