let f be PVertexMapping of G1,G2; ( f is isomorphism implies ( f is total & f is one-to-one & f is onto & f is continuous ) )
assume A1:
f is isomorphism
; ( 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 )
; f is continuous
now 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,G1let v,
w,
e9 be
object ;
( 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 )
;
ex e being object st e Joins v,w,G1then 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;
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;
verum end;
hence
f is continuous
by Th2; verum