theorem :: GLIB_010:178
for G1, G2 being loopless _trivial _Graph holds
( G2 is G1 -Disomorphic & G2 is G1 -isomorphic )