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

proof

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

end;

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

proof

assume A4: G .allSG() is loopless ; :: thesis:
G is GraphUnion of G .allSG() by Th35;
hence G is loopless by A4; :: thesis:

end;

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

proof

assume A6: G is non-multi ; :: thesis:

now :: thesis:

let H be _Graph; :: thesis:
assume H in G .allSG() ; :: thesis:
then H is Subgraph of G by Th1;
hence H is non-multi by A6; :: thesis:

end;

hence G .allSG() is non-multi by GLIB_014:def 4; :: thesis:

end;

thus A7: ( G .allSG() is non-multi implies G is non-multi ) :: thesis:

proof

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

end;

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

proof

assume A11: G is non-Dmulti ; :: thesis:

now :: thesis:

let H be _Graph; :: thesis:
assume H in G .allSG() ; :: thesis:
then H is Subgraph of G by Th1;
hence H is non-Dmulti by A11; :: thesis:

end;

hence G .allSG() is non-Dmulti by GLIB_014:def 5; :: thesis:

end;

thus A12: ( G .allSG() is non-Dmulti implies G is non-Dmulti ) :: thesis:

proof

assume A13: G .allSG() is non-Dmulti ; :: thesis:
G | _GraphSelectors in G .allSG() by Th3;
then A14: G | _GraphSelectors is non-Dmulti by A13;
G == G | _GraphSelectors by GLIB_000:128;
hence G is non-Dmulti by A14, GLIB_000:89; :: thesis:

end;

thus ( G is simple implies G .allSG() is simple ) by A1, A5; :: thesis:
thus ( G .allSG() is simple implies G is simple ) by A3, A7; :: thesis:
thus ( G is Dsimple implies G .allSG() is Dsimple ) by A1, A10; :: thesis:
thus ( G .allSG() is Dsimple implies G is Dsimple ) by A3, A12; :: thesis:

hereby :: thesis:

assume A15: G is acyclic ; :: thesis:

now :: thesis:

let H be _Graph; :: thesis:
assume H in G .allSG() ; :: thesis:
then H is Subgraph of G by Th1;
hence H is acyclic by A15; :: thesis:

end;

hence G .allSG() is acyclic by GLIB_014:def 8; :: thesis:

end;

hereby :: thesis:

assume A16: G .allSG() is acyclic ; :: thesis:
G | _GraphSelectors in G .allSG() by Th3;
then A17: G | _GraphSelectors is acyclic by A16;
G == G | _GraphSelectors by GLIB_000:128;
hence G is acyclic by A17, GLIB_002:44; :: thesis:

end;

hereby :: thesis:

assume A18: G is edgeless ; :: thesis:

now :: thesis:

let H be _Graph; :: thesis:
assume H in G .allSG() ; :: thesis:
then H is Subgraph of G by Th1;
hence H is edgeless by A18; :: thesis:

end;

hence G .allSG() is edgeless by GLIB_014:def 12; :: thesis:

end;

hereby :: thesis:

assume A19: G .allSG() is edgeless ; :: thesis:
G | _GraphSelectors in G .allSG() by Th3;
then A20: G | _GraphSelectors is edgeless by A19;
G == G | _GraphSelectors by GLIB_000:128;
hence G is edgeless by A20, GLIB_008:52; :: thesis:

end;