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

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

let v, w, e9 be object ; :: thesis: ( v in dom f & w in dom f & e9 Joins f . v,f . w,G2 implies ex e being object st e Joins v,w,G1 )
assume A2: ( v in dom f & w in dom f & e9 Joins f . v,f . w,G2 ) ; :: thesis: ex e being object st e Joins 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 SJoins {(f . v)},{(f . w)},G2 by A2, GLIB_000:17;
then e9 in G2 .edgesBetween ({(f . v)},{(f . w)}) by GLIB_000:def 30;
then card (G2 .edgesBetween ({(f . v0)},{(f . w0)})) <> 0 ;
then card (G1 .edgesBetween ({v0},{w0})) <> 0 by A1;
then G1 .edgesBetween ({v0},{w0}) <> {} ;
then consider e being object such that
A3: e in G1 .edgesBetween ({v0},{w0}) by XBOOLE_0:def 1;
take e = e; :: thesis: e Joins v,w,G1
e SJoins {v},{w},G1 by A3, GLIB_000:def 30;
then ( e in the_Edges_of G1 & ( ( (the_Source_of G1) . e in {v} & (the_Target_of G1) . e in {w} ) or ( (the_Source_of G1) . e in {w} & (the_Target_of G1) . e in {v} ) ) ) by GLIB_000:def 15;
then ( e in the_Edges_of G1 & ( ( (the_Source_of G1) . e = v & (the_Target_of G1) . e = w ) or ( (the_Source_of G1) . e = w & (the_Target_of G1) . e = v ) ) ) by TARSKI:def 1;
hence e Joins v,w,G1 by GLIB_000:def 13; :: thesis: verum

end;

hence f is continuous by Th2; :: thesis: verum