let G be _Graph; :: thesis: ( ( G is loopless implies G .allSpanningSG() is loopless ) & ( G .allSpanningSG() is loopless implies G is loopless ) & ( G is non-multi implies G .allSpanningSG() is non-multi ) & ( G .allSpanningSG() is non-multi implies G is non-multi ) & ( G is non-Dmulti implies G .allSpanningSG() is non-Dmulti ) & ( G .allSpanningSG() is non-Dmulti implies G is non-Dmulti ) & ( G is simple implies G .allSpanningSG() is simple ) & ( G .allSpanningSG() is simple implies G is simple ) & ( G is Dsimple implies G .allSpanningSG() is Dsimple ) & ( G .allSpanningSG() is Dsimple implies G is Dsimple ) & ( G is acyclic implies G .allSpanningSG() is acyclic ) & ( G .allSpanningSG() is acyclic implies G is acyclic ) & ( G is edgeless implies G .allSpanningSG() is edgeless ) & ( G .allSpanningSG() is edgeless implies G is edgeless ) )
thus ( G is loopless implies G .allSpanningSG() is loopless ) ; :: thesis: ( ( G .allSpanningSG() is loopless implies G is loopless ) & ( G is non-multi implies G .allSpanningSG() is non-multi ) & ( G .allSpanningSG() is non-multi implies G is non-multi ) & ( G is non-Dmulti implies G .allSpanningSG() is non-Dmulti ) & ( G .allSpanningSG() is non-Dmulti implies G is non-Dmulti ) & ( G is simple implies G .allSpanningSG() is simple ) & ( G .allSpanningSG() is simple implies G is simple ) & ( G is Dsimple implies G .allSpanningSG() is Dsimple ) & ( G .allSpanningSG() is Dsimple implies G is Dsimple ) & ( G is acyclic implies G .allSpanningSG() is acyclic ) & ( G .allSpanningSG() is acyclic implies G is acyclic ) & ( G is edgeless implies G .allSpanningSG() is edgeless ) & ( G .allSpanningSG() is edgeless implies G is edgeless ) )
thus A1: ( G .allSpanningSG() is loopless implies G is loopless ) :: thesis: ( ( G is non-multi implies G .allSpanningSG() is non-multi ) & ( G .allSpanningSG() is non-multi implies G is non-multi ) & ( G is non-Dmulti implies G .allSpanningSG() is non-Dmulti ) & ( G .allSpanningSG() is non-Dmulti implies G is non-Dmulti ) & ( G is simple implies G .allSpanningSG() is simple ) & ( G .allSpanningSG() is simple implies G is simple ) & ( G is Dsimple implies G .allSpanningSG() is Dsimple ) & ( G .allSpanningSG() is Dsimple implies G is Dsimple ) & ( G is acyclic implies G .allSpanningSG() is acyclic ) & ( G .allSpanningSG() is acyclic implies G is acyclic ) & ( G is edgeless implies G .allSpanningSG() is edgeless ) & ( G .allSpanningSG() is edgeless implies G is edgeless ) )

proof

assume A2: G .allSpanningSG() is loopless ; :: thesis: G is loopless
G is GraphUnion of G .allSpanningSG() by Th72;
hence G is loopless by A2; :: thesis: verum

end;

thus ( G is non-multi implies G .allSpanningSG() is non-multi ) ; :: thesis: ( ( G .allSpanningSG() is non-multi implies G is non-multi ) & ( G is non-Dmulti implies G .allSpanningSG() is non-Dmulti ) & ( G .allSpanningSG() is non-Dmulti implies G is non-Dmulti ) & ( G is simple implies G .allSpanningSG() is simple ) & ( G .allSpanningSG() is simple implies G is simple ) & ( G is Dsimple implies G .allSpanningSG() is Dsimple ) & ( G .allSpanningSG() is Dsimple implies G is Dsimple ) & ( G is acyclic implies G .allSpanningSG() is acyclic ) & ( G .allSpanningSG() is acyclic implies G is acyclic ) & ( G is edgeless implies G .allSpanningSG() is edgeless ) & ( G .allSpanningSG() is edgeless implies G is edgeless ) )
thus A3: ( G .allSpanningSG() is non-multi implies G is non-multi ) :: thesis: ( ( G is non-Dmulti implies G .allSpanningSG() is non-Dmulti ) & ( G .allSpanningSG() is non-Dmulti implies G is non-Dmulti ) & ( G is simple implies G .allSpanningSG() is simple ) & ( G .allSpanningSG() is simple implies G is simple ) & ( G is Dsimple implies G .allSpanningSG() is Dsimple ) & ( G .allSpanningSG() is Dsimple implies G is Dsimple ) & ( G is acyclic implies G .allSpanningSG() is acyclic ) & ( G .allSpanningSG() is acyclic implies G is acyclic ) & ( G is edgeless implies G .allSpanningSG() is edgeless ) & ( G .allSpanningSG() is edgeless implies G is edgeless ) )

proof

assume A4: G .allSpanningSG() is non-multi ; :: thesis: G is non-multi
G | _GraphSelectors in G .allSpanningSG() by Th62;
then A5: G | _GraphSelectors is non-multi by A4;
G == G | _GraphSelectors by GLIB_000:128;
hence G is non-multi by A5, GLIB_000:89; :: thesis: verum

end;

thus ( G is non-Dmulti implies G .allSpanningSG() is non-Dmulti ) ; :: thesis: ( ( G .allSpanningSG() is non-Dmulti implies G is non-Dmulti ) & ( G is simple implies G .allSpanningSG() is simple ) & ( G .allSpanningSG() is simple implies G is simple ) & ( G is Dsimple implies G .allSpanningSG() is Dsimple ) & ( G .allSpanningSG() is Dsimple implies G is Dsimple ) & ( G is acyclic implies G .allSpanningSG() is acyclic ) & ( G .allSpanningSG() is acyclic implies G is acyclic ) & ( G is edgeless implies G .allSpanningSG() is edgeless ) & ( G .allSpanningSG() is edgeless implies G is edgeless ) )
thus A6: ( G .allSpanningSG() is non-Dmulti implies G is non-Dmulti ) :: thesis: ( ( G is simple implies G .allSpanningSG() is simple ) & ( G .allSpanningSG() is simple implies G is simple ) & ( G is Dsimple implies G .allSpanningSG() is Dsimple ) & ( G .allSpanningSG() is Dsimple implies G is Dsimple ) & ( G is acyclic implies G .allSpanningSG() is acyclic ) & ( G .allSpanningSG() is acyclic implies G is acyclic ) & ( G is edgeless implies G .allSpanningSG() is edgeless ) & ( G .allSpanningSG() is edgeless implies G is edgeless ) )

proof

assume A7: G .allSpanningSG() is non-Dmulti ; :: thesis: G is non-Dmulti
G | _GraphSelectors in G .allSpanningSG() by Th62;
then A8: G | _GraphSelectors is non-Dmulti by A7;
G == G | _GraphSelectors by GLIB_000:128;
hence G is non-Dmulti by A8, GLIB_000:89; :: thesis: verum

end;

thus ( G is simple implies G .allSpanningSG() is simple ) ; :: thesis: ( ( G .allSpanningSG() is simple implies G is simple ) & ( G is Dsimple implies G .allSpanningSG() is Dsimple ) & ( G .allSpanningSG() is Dsimple implies G is Dsimple ) & ( G is acyclic implies G .allSpanningSG() is acyclic ) & ( G .allSpanningSG() is acyclic implies G is acyclic ) & ( G is edgeless implies G .allSpanningSG() is edgeless ) & ( G .allSpanningSG() is edgeless implies G is edgeless ) )
thus ( G .allSpanningSG() is simple implies G is simple ) by A1, A3; :: thesis: ( ( G is Dsimple implies G .allSpanningSG() is Dsimple ) & ( G .allSpanningSG() is Dsimple implies G is Dsimple ) & ( G is acyclic implies G .allSpanningSG() is acyclic ) & ( G .allSpanningSG() is acyclic implies G is acyclic ) & ( G is edgeless implies G .allSpanningSG() is edgeless ) & ( G .allSpanningSG() is edgeless implies G is edgeless ) )
thus ( G is Dsimple implies G .allSpanningSG() is Dsimple ) ; :: thesis: ( ( G .allSpanningSG() is Dsimple implies G is Dsimple ) & ( G is acyclic implies G .allSpanningSG() is acyclic ) & ( G .allSpanningSG() is acyclic implies G is acyclic ) & ( G is edgeless implies G .allSpanningSG() is edgeless ) & ( G .allSpanningSG() is edgeless implies G is edgeless ) )
thus ( G .allSpanningSG() is Dsimple implies G is Dsimple ) by A1, A6; :: thesis: ( ( G is acyclic implies G .allSpanningSG() is acyclic ) & ( G .allSpanningSG() is acyclic implies G is acyclic ) & ( G is edgeless implies G .allSpanningSG() is edgeless ) & ( G .allSpanningSG() is edgeless implies G is edgeless ) )
thus ( G is acyclic implies G .allSpanningSG() is acyclic ) ; :: thesis: ( ( G .allSpanningSG() is acyclic implies G is acyclic ) & ( G is edgeless implies G .allSpanningSG() is edgeless ) & ( G .allSpanningSG() is edgeless implies G is edgeless ) )

hereby :: thesis: ( G is edgeless iff G .allSpanningSG() is edgeless )

assume A9: G .allSpanningSG() is acyclic ; :: thesis: G is acyclic
G | _GraphSelectors in G .allSpanningSG() by Th62;
then A10: G | _GraphSelectors is acyclic by A9;
G == G | _GraphSelectors by GLIB_000:128;
hence G is acyclic by A10, GLIB_002:44; :: thesis: verum

end;

thus ( G is edgeless implies G .allSpanningSG() is edgeless ) ; :: thesis: ( G .allSpanningSG() is edgeless implies G is edgeless )

hereby :: thesis: verum

assume A11: G .allSpanningSG() is edgeless ; :: thesis: G is edgeless
G | _GraphSelectors in G .allSpanningSG() by Th62;
then A12: G | _GraphSelectors is edgeless by A11;
G == G | _GraphSelectors by GLIB_000:128;
hence G is edgeless by A12, GLIB_008:52; :: thesis: verum

end;