let G1, G2 be non-Dmulti _Graph; :: thesis: ( G2 is G1 -Disomorphic iff ex f being directed PVertexMapping of G1,G2 st f is Disomorphism )

hereby :: thesis: ( ex f being directed PVertexMapping of G1,G2 st f is Disomorphism implies G2 is G1 -Disomorphic )

assume G2 is G1 -Disomorphic ; :: thesis: ex f being directed PVertexMapping of G1,G2 st f is Disomorphism
then consider F being PGraphMapping of G1,G2 such that
A1: F is Disomorphism by GLIB_010:def 24;
consider f being directed PVertexMapping of G1,G2 such that
A2: ( F _V = f & f is Disomorphism ) by A1, Th26;
take f = f; :: thesis: f is Disomorphism
thus f is Disomorphism by A2; :: thesis: verum

end;

given f being directed PVertexMapping of G1,G2 such that A3: f is Disomorphism ; :: thesis: G2 is G1 -Disomorphic
DPVM2PGM f is Disomorphism by A3, Th48;
hence G2 is G1 -Disomorphic by GLIB_010:def 24; :: thesis: verum