let G be _Graph; :: thesis: ( G is G -Disomorphic & G is G -isomorphic )

( id G is directed & id G is strong_SG-embedding & id G is isomorphism ) ;

hence ( G is G -Disomorphic & G is G -isomorphic ) ; :: thesis: verum

( id G is directed & id G is strong_SG-embedding & id G is isomorphism ) ;

hence ( G is G -Disomorphic & G is G -isomorphic ) ; :: thesis: verum