let G1, G2 be loopless _trivial _Graph; :: thesis: ( G2 is G1 -Disomorphic & G2 is G1 -isomorphic )
set F = the non empty PGraphMapping of G1,G2;
( the non empty PGraphMapping of G1,G2 is directed & the non empty PGraphMapping of G1,G2 is isomorphism ) ;
hence G2 is G1 -Disomorphic ; :: thesis: G2 is G1 -isomorphic
hence G2 is G1 -isomorphic ; :: thesis: verum