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

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