theorem Th3: :: GLIB_014:3

for F being Graph-yielding Function holds
( ( F is plain implies rng F is plain ) & ( rng F is plain implies F is plain ) & ( F is loopless implies rng F is loopless ) & ( rng F is loopless implies F is loopless ) & ( F is non-multi implies rng F is non-multi ) & ( rng F is non-multi implies F is non-multi ) & ( F is non-Dmulti implies rng F is non-Dmulti ) & ( rng F is non-Dmulti implies F is non-Dmulti ) & ( F is acyclic implies rng F is acyclic ) & ( rng F is acyclic implies F is acyclic ) & ( F is connected implies rng F is connected ) & ( rng F is connected implies F is connected ) & ( F is chordal implies rng F is chordal ) & ( rng F is chordal implies F is chordal ) & ( F is edgeless implies rng F is edgeless ) & ( rng F is edgeless implies F is edgeless ) & ( F is loopfull implies rng F is loopfull ) & ( rng F is loopfull implies F is loopfull ) )