let f be PVertexMapping of G1,G2; :: thesis: ( f is Disomorphism implies ( f is total & f is one-to-one & f is onto & f is isomorphism & f is continuous & f is directed & f is Dcontinuous ) )
assume A4: f is Disomorphism ; :: thesis: ( f is total & f is one-to-one & f is onto & f is isomorphism & f is continuous & f is directed & f is Dcontinuous )
hence ( f is total & f is one-to-one & f is onto ) ; :: thesis: ( f is isomorphism & f is continuous & f is directed & f is Dcontinuous )

now :: thesis: for v, w being Vertex of G1 holds card (G1 .edgesBetween ({v},{w})) = card (G2 .edgesBetween ({(f . v)},{(f . w)}))

let v, w be Vertex of G1; :: thesis: card (G1 .edgesBetween ({b₁},{b₂})) = card (G2 .edgesBetween ({(f . b₁)},{(f . b₂)}))

per cases ( v <> w or v = w ) ;

suppose A5: v <> w ; :: thesis: card (G1 .edgesBetween ({b₁},{b₂})) = card (G2 .edgesBetween ({(f . b₁)},{(f . b₂)}))

then A6: f . v <> f . w by A4, FUNCT_2:19;
thus card (G1 .edgesBetween ({v},{w})) = card ((G1 .edgesDBetween ({v},{w})) \/ (G1 .edgesDBetween ({w},{v}))) by A5, GLIB_000:133
.= (card (G1 .edgesDBetween ({v},{w}))) +` (card (G1 .edgesDBetween ({w},{v}))) by A5, GLIB_000:133, CARD_2:35
.= (card (G1 .edgesDBetween ({v},{w}))) +` (card (G2 .edgesDBetween ({(f . w)},{(f . v)}))) by A4
.= (card (G2 .edgesDBetween ({(f . v)},{(f . w)}))) +` (card (G2 .edgesDBetween ({(f . w)},{(f . v)}))) by A4
.= card ((G2 .edgesDBetween ({(f . v)},{(f . w)})) \/ (G2 .edgesDBetween ({(f . w)},{(f . v)}))) by A6, GLIB_000:133, CARD_2:35
.= card (G2 .edgesBetween ({(f . v)},{(f . w)})) by A6, GLIB_000:133 ; :: thesis: verum

end;

suppose A7: v = w ; :: thesis: card (G1 .edgesBetween ({b₁},{b₂})) = card (G2 .edgesBetween ({(f . b₁)},{(f . b₂)}))

thus card (G1 .edgesBetween ({v},{w})) = card (G1 .edgesDBetween ({v},{w})) by A7, GLIB_000:134
.= card (G2 .edgesDBetween ({(f . v)},{(f . w)})) by A4
.= card (G2 .edgesBetween ({(f . v)},{(f . w)})) by A7, GLIB_000:134 ; :: thesis: verum

end;

end;

end;

hence f is isomorphism by A4; :: thesis: ( f is continuous & f is directed & f is Dcontinuous )
hence f is continuous ; :: thesis: ( f is directed & f is Dcontinuous )

now :: thesis: for v, w, e being object st v in dom f & w in dom f & e DJoins v,w,G1 holds
ex e9 being object st e9 DJoins f . v,f . w,G2

let v, w, e be object ; :: thesis: ( v in dom f & w in dom f & e DJoins v,w,G1 implies ex e9 being object st e9 DJoins f . v,f . w,G2 )
assume A8: ( v in dom f & w in dom f & e DJoins v,w,G1 ) ; :: thesis: ex e9 being object st e9 DJoins f . v,f . w,G2
then reconsider v0 = v, w0 = w as Vertex of G1 ;
( v in {v} & w in {w} ) by TARSKI:def 1;
then e DSJoins {v},{w},G1 by A8, GLIB_000:126;
then e in G1 .edgesDBetween ({v},{w}) by GLIB_000:def 31;
then card (G1 .edgesDBetween ({v0},{w0})) <> 0 ;
then card (G2 .edgesDBetween ({(f . v0)},{(f . w0)})) <> 0 by A4;
then G2 .edgesDBetween ({(f . v)},{(f . w)}) <> {} ;
then consider e9 being object such that
A9: e9 in G2 .edgesDBetween ({(f . v)},{(f . w)}) by XBOOLE_0:def 1;
take e9 = e9; :: thesis: e9 DJoins f . v,f . w,G2
e9 DSJoins {(f . v)},{(f . w)},G2 by A9, GLIB_000:def 31;
then ( e9 in the_Edges_of G2 & (the_Source_of G2) . e9 in {(f . v)} & (the_Target_of G2) . e9 in {(f . w)} ) by GLIB_000:def 16;
then ( e9 in the_Edges_of G2 & (the_Source_of G2) . e9 = f . v & (the_Target_of G2) . e9 = f . w ) by TARSKI:def 1;
hence e9 DJoins f . v,f . w,G2 by GLIB_000:def 14; :: thesis: verum

end;

hence f is directed ; :: thesis: f is Dcontinuous

now :: thesis: for v, w, e9 being object st v in dom f & w in dom f & e9 DJoins f . v,f . w,G2 holds
ex e being object st e DJoins v,w,G1

let v, w, e9 be object ; :: thesis: ( v in dom f & w in dom f & e9 DJoins f . v,f . w,G2 implies ex e being object st e DJoins v,w,G1 )
assume A10: ( v in dom f & w in dom f & e9 DJoins f . v,f . w,G2 ) ; :: thesis: ex e being object st e DJoins v,w,G1
then reconsider v0 = v, w0 = w as Vertex of G1 ;
( f . v in {(f . v)} & f . w in {(f . w)} ) by TARSKI:def 1;
then e9 DSJoins {(f . v)},{(f . w)},G2 by A10, GLIB_000:126;
then e9 in G2 .edgesDBetween ({(f . v)},{(f . w)}) by GLIB_000:def 31;
then card (G2 .edgesDBetween ({(f . v0)},{(f . w0)})) <> 0 ;
then card (G1 .edgesDBetween ({v0},{w0})) <> 0 by A4;
then G1 .edgesDBetween ({v},{w}) <> {} ;
then consider e being object such that
A11: e in G1 .edgesDBetween ({v},{w}) by XBOOLE_0:def 1;
take e = e; :: thesis: e DJoins v,w,G1
e DSJoins {v},{w},G1 by A11, GLIB_000:def 31;
then ( e in the_Edges_of G1 & (the_Source_of G1) . e in {v} & (the_Target_of G1) . e in {w} ) by GLIB_000:def 16;
then ( e in the_Edges_of G1 & (the_Source_of G1) . e = v & (the_Target_of G1) . e = w ) by TARSKI:def 1;
hence e DJoins v,w,G1 by GLIB_000:def 14; :: thesis: verum

end;

hence f is Dcontinuous ; :: thesis: verum