let G be _Graph; :: thesis:
thus A1: ( G is loopless implies G .allInducedSG() is loopless ) :: thesis:

proof

assume A2: G is loopless ; :: thesis:
G is GraphUnion of G .allInducedSG() by Th55;
hence G .allInducedSG() is loopless by A2, GLIB_014:23; :: thesis:

end;

thus A3: ( G .allInducedSG() is loopless implies G is loopless ) :: thesis:

proof

assume A4: G .allInducedSG() is loopless ; :: thesis:
G is GraphUnion of G .allInducedSG() by Th55;
hence G is loopless by A4; :: thesis:

end;

thus A5: ( G is non-multi implies G .allInducedSG() is non-multi ) :: thesis:

proof

assume G is non-multi ; :: thesis:
then G .allSG() is non-multi ;
hence G .allInducedSG() is non-multi ; :: thesis:

end;

thus A6: ( G .allInducedSG() is non-multi implies G is non-multi ) :: thesis:

proof

assume A7: G .allInducedSG() is non-multi ; :: thesis:
G | _GraphSelectors in G .allInducedSG() by Th47;
then A8: G | _GraphSelectors is non-multi by A7;
G == G | _GraphSelectors by GLIB_000:128;
hence G is non-multi by A8, GLIB_000:89; :: thesis:

end;

thus A9: ( G is non-Dmulti implies G .allInducedSG() is non-Dmulti ) :: thesis:

proof

assume G is non-Dmulti ; :: thesis:
then G .allSG() is non-Dmulti ;
hence G .allInducedSG() is non-Dmulti ; :: thesis:

end;

thus A10: ( G .allInducedSG() is non-Dmulti implies G is non-Dmulti ) :: thesis:

proof

assume A11: G .allInducedSG() is non-Dmulti ; :: thesis:
G | _GraphSelectors in G .allInducedSG() by Th47;
then A12: G | _GraphSelectors is non-Dmulti by A11;
G == G | _GraphSelectors by GLIB_000:128;
hence G is non-Dmulti by A12, GLIB_000:89; :: thesis:

end;

thus ( G is simple implies G .allInducedSG() is simple ) by A1, A5; :: thesis:
thus ( G .allInducedSG() is simple implies G is simple ) by A3, A6; :: thesis:
thus ( G is Dsimple implies G .allInducedSG() is Dsimple ) by A1, A9; :: thesis:
thus ( G .allInducedSG() is Dsimple implies G is Dsimple ) by A3, A10; :: thesis:

hereby :: thesis:

assume G is acyclic ; :: thesis:
then G .allSG() is acyclic ;
hence G .allInducedSG() is acyclic ; :: thesis:

end;

hereby :: thesis:

assume A13: G .allInducedSG() is acyclic ; :: thesis:
G | _GraphSelectors in G .allInducedSG() by Th47;
then A14: G | _GraphSelectors is acyclic by A13;
G == G | _GraphSelectors by GLIB_000:128;
hence G is acyclic by A14, GLIB_002:44; :: thesis:

end;

hereby :: thesis:

assume G is edgeless ; :: thesis:
then G .allSG() is edgeless ;
hence G .allInducedSG() is edgeless ; :: thesis:

end;

hereby :: thesis:

assume A15: G .allInducedSG() is edgeless ; :: thesis:
G | _GraphSelectors in G .allInducedSG() by Th47;
then A16: G | _GraphSelectors is edgeless by A15;
G == G | _GraphSelectors by GLIB_000:128;
hence G is edgeless by A16, GLIB_008:52; :: thesis:

end;

hereby :: thesis:

assume A17: G is chordal ; :: thesis:

now :: thesis:

let H be _Graph; :: thesis:
assume H in G .allInducedSG() ; :: thesis:
then consider V being non empty Subset of (the_Vertices_of G) such that
A18: H is plain inducedSubgraph of G,V by Th45;
thus H is chordal by A17, A18; :: thesis:

end;

hence G .allInducedSG() is chordal by GLIB_014:def 11; :: thesis:

end;

hereby :: thesis:

assume A19: G .allInducedSG() is chordal ; :: thesis:
G | _GraphSelectors in G .allInducedSG() by Th47;
then A20: G | _GraphSelectors is chordal by A19;
G == G | _GraphSelectors by GLIB_000:128;
hence G is chordal by A20, CHORD:95; :: thesis:

end;

hereby :: thesis:

assume A21: G is loopfull ; :: thesis:

now :: thesis:

let H be _Graph; :: thesis:
assume H in G .allInducedSG() ; :: thesis:
then consider V being non empty Subset of (the_Vertices_of G) such that
A22: H is plain inducedSubgraph of G,V by Th45;
thus H is loopfull by A21, A22; :: thesis:

end;

hence G .allInducedSG() is loopfull by GLIB_014:def 13; :: thesis:

end;

hereby :: thesis:

assume A23: G .allInducedSG() is loopfull ; :: thesis:
G | _GraphSelectors in G .allInducedSG() by Th47;
then A24: G | _GraphSelectors is loopfull by A23;
G == G | _GraphSelectors by GLIB_000:128;
hence G is loopfull by A24, GLIB_012:4; :: thesis:

end;