let H be _Graph; :: thesis: ( H is G -Disomorphic implies H is Dcomplete )
assume H is G -Disomorphic ; :: thesis: H is Dcomplete
then consider F being PGraphMapping of G,H such that
A1: F is Disomorphism by GLIB_010:def 24;
thus H is Dcomplete by A1, Th10; :: thesis: verum