take G ; :: thesis: ( G is G -Disomorphic & G is G -isomorphic )
( id G is directed & id G is isomorphism ) ;
hence ( G is G -Disomorphic & G is G -isomorphic ) ; :: thesis: verum