for S1, S2 being Graph-membered set st S1,S2 are_isomorphic holds
( ( S1 is empty implies S2 is empty ) & ( S1 is loopless implies S2 is loopless ) & ( S1 is non-multi implies S2 is non-multi ) & ( S1 is simple implies S2 is simple ) & ( S1 is acyclic implies S2 is acyclic ) & ( S1 is connected implies S2 is connected ) & ( S1 is Tree-like implies S2 is Tree-like ) & ( S1 is chordal implies S2 is chordal ) & ( S1 is edgeless implies S2 is edgeless ) & ( S1 is loopfull implies S2 is loopfull ) )