for F1, F2 being Graph-yielding Function st F1,F2 are_isomorphic holds
( ( F1 is empty implies F2 is empty ) & ( F1 is loopless implies F2 is loopless ) & ( F1 is non-multi implies F2 is non-multi ) & ( F1 is simple implies F2 is simple ) & ( F1 is acyclic implies F2 is acyclic ) & ( F1 is connected implies F2 is connected ) & ( F1 is Tree-like implies F2 is Tree-like ) & ( F1 is chordal implies F2 is chordal ) & ( F1 is edgeless implies F2 is edgeless ) & ( F1 is loopfull implies F2 is loopfull ) )