let G be _Graph; :: thesis: ( ( G is loopless implies G .allComponents() is loopless ) & ( G .allComponents() is loopless implies G is loopless ) & ( G is non-multi implies G .allComponents() is non-multi ) & ( G .allComponents() is non-multi implies G is non-multi ) & ( G is non-Dmulti implies G .allComponents() is non-Dmulti ) & ( G .allComponents() is non-Dmulti implies G is non-Dmulti ) & ( G is simple implies G .allComponents() is simple ) & ( G .allComponents() is simple implies G is simple ) & ( G is Dsimple implies G .allComponents() is Dsimple ) & ( G .allComponents() is Dsimple implies G is Dsimple ) & ( G is acyclic implies G .allComponents() is acyclic ) & ( G .allComponents() is acyclic implies G is acyclic ) & ( G is edgeless implies G .allComponents() is edgeless ) & ( G .allComponents() is edgeless implies G is edgeless ) & ( G is chordal implies G .allComponents() is chordal ) & ( G .allComponents() is chordal implies G is chordal ) & ( G is loopfull implies G .allComponents() is loopfull ) & ( G .allComponents() is loopfull implies G is loopfull ) )
A1: G is GraphUnion of G .allComponents() by Th198;
thus ( G is loopless iff G .allComponents() is loopless ) by A1; :: thesis: ( ( G is non-multi implies G .allComponents() is non-multi ) & ( G .allComponents() is non-multi implies G is non-multi ) & ( G is non-Dmulti implies G .allComponents() is non-Dmulti ) & ( G .allComponents() is non-Dmulti implies G is non-Dmulti ) & ( G is simple implies G .allComponents() is simple ) & ( G .allComponents() is simple implies G is simple ) & ( G is Dsimple implies G .allComponents() is Dsimple ) & ( G .allComponents() is Dsimple implies G is Dsimple ) & ( G is acyclic implies G .allComponents() is acyclic ) & ( G .allComponents() is acyclic implies G is acyclic ) & ( G is edgeless implies G .allComponents() is edgeless ) & ( G .allComponents() is edgeless implies G is edgeless ) & ( G is chordal implies G .allComponents() is chordal ) & ( G .allComponents() is chordal implies G is chordal ) & ( G is loopfull implies G .allComponents() is loopfull ) & ( G .allComponents() is loopfull implies G is loopfull ) )
thus ( G is non-multi iff G .allComponents() is non-multi ) by A1; :: thesis: ( ( G is non-Dmulti implies G .allComponents() is non-Dmulti ) & ( G .allComponents() is non-Dmulti implies G is non-Dmulti ) & ( G is simple implies G .allComponents() is simple ) & ( G .allComponents() is simple implies G is simple ) & ( G is Dsimple implies G .allComponents() is Dsimple ) & ( G .allComponents() is Dsimple implies G is Dsimple ) & ( G is acyclic implies G .allComponents() is acyclic ) & ( G .allComponents() is acyclic implies G is acyclic ) & ( G is edgeless implies G .allComponents() is edgeless ) & ( G .allComponents() is edgeless implies G is edgeless ) & ( G is chordal implies G .allComponents() is chordal ) & ( G .allComponents() is chordal implies G is chordal ) & ( G is loopfull implies G .allComponents() is loopfull ) & ( G .allComponents() is loopfull implies G is loopfull ) )
thus ( G is non-Dmulti iff G .allComponents() is non-Dmulti ) by A1; :: thesis: ( ( G is simple implies G .allComponents() is simple ) & ( G .allComponents() is simple implies G is simple ) & ( G is Dsimple implies G .allComponents() is Dsimple ) & ( G .allComponents() is Dsimple implies G is Dsimple ) & ( G is acyclic implies G .allComponents() is acyclic ) & ( G .allComponents() is acyclic implies G is acyclic ) & ( G is edgeless implies G .allComponents() is edgeless ) & ( G .allComponents() is edgeless implies G is edgeless ) & ( G is chordal implies G .allComponents() is chordal ) & ( G .allComponents() is chordal implies G is chordal ) & ( G is loopfull implies G .allComponents() is loopfull ) & ( G .allComponents() is loopfull implies G is loopfull ) )
thus ( G is simple iff G .allComponents() is simple ) by A1; :: thesis: ( ( G is Dsimple implies G .allComponents() is Dsimple ) & ( G .allComponents() is Dsimple implies G is Dsimple ) & ( G is acyclic implies G .allComponents() is acyclic ) & ( G .allComponents() is acyclic implies G is acyclic ) & ( G is edgeless implies G .allComponents() is edgeless ) & ( G .allComponents() is edgeless implies G is edgeless ) & ( G is chordal implies G .allComponents() is chordal ) & ( G .allComponents() is chordal implies G is chordal ) & ( G is loopfull implies G .allComponents() is loopfull ) & ( G .allComponents() is loopfull implies G is loopfull ) )
thus ( G is Dsimple iff G .allComponents() is Dsimple ) by A1; :: thesis: ( ( G is acyclic implies G .allComponents() is acyclic ) & ( G .allComponents() is acyclic implies G is acyclic ) & ( G is edgeless implies G .allComponents() is edgeless ) & ( G .allComponents() is edgeless implies G is edgeless ) & ( G is chordal implies G .allComponents() is chordal ) & ( G .allComponents() is chordal implies G is chordal ) & ( G is loopfull implies G .allComponents() is loopfull ) & ( G .allComponents() is loopfull implies G is loopfull ) )
thus ( G is acyclic iff G .allComponents() is acyclic ) by A1; :: thesis: ( ( G is edgeless implies G .allComponents() is edgeless ) & ( G .allComponents() is edgeless implies G is edgeless ) & ( G is chordal implies G .allComponents() is chordal ) & ( G .allComponents() is chordal implies G is chordal ) & ( G is loopfull implies G .allComponents() is loopfull ) & ( G .allComponents() is loopfull implies G is loopfull ) )
thus ( G is edgeless iff G .allComponents() is edgeless ) by A1; :: thesis: ( ( G is chordal implies G .allComponents() is chordal ) & ( G .allComponents() is chordal implies G is chordal ) & ( G is loopfull implies G .allComponents() is loopfull ) & ( G .allComponents() is loopfull implies G is loopfull ) )
thus ( G is chordal iff G .allComponents() is chordal ) by A1, GLIB_015:63; :: thesis: ( G is loopfull iff G .allComponents() is loopfull )
thus ( G is loopfull iff G .allComponents() is loopfull ) by A1, GLIB_015:63; :: thesis: verum