:: deftheorem defines is_isomorphic_to SGRAPH1:def 5 :
for X being set
for G, G9 being SimpleGraph of X holds
( G is_isomorphic_to G9 iff ex Fv being Function of the carrier of G, the carrier of G9 st
( Fv is bijective & ( for v1, v2 being Element of G holds
( {v1,v2} in the SEdges of G iff {(Fv . v1),(Fv . v2)} in the SEdges of G ) ) ) );