let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is Disomorphism holds
( G1 is Dcomplete iff G2 is Dcomplete )
let F be PGraphMapping of G1,G2; :: thesis: ( F is Disomorphism implies ( G1 is Dcomplete iff G2 is Dcomplete ) )
assume A1: F is Disomorphism ; :: thesis: ( G1 is Dcomplete iff G2 is Dcomplete )
then reconsider F0 = F as one-to-one PGraphMapping of G1,G2 ;
( F0 " is isomorphism & F0 " is Dcontinuous ) by A1, GLIB_010:74, GLIB_010:75;
hence ( G1 is Dcomplete implies G2 is Dcomplete ) by Th9; :: thesis: ( G2 is Dcomplete implies G1 is Dcomplete )
thus ( G2 is Dcomplete implies G1 is Dcomplete ) by A1, Th9; :: thesis: verum