let G1, G2 be _Graph; for f being PVertexMapping of G1,G2 holds
( f is continuous iff 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 f be PVertexMapping of G1,G2; ( f is continuous iff 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 )
hereby ( ( 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 ) implies f is continuous )
assume A1:
f is
continuous
;
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 /. v0 = f . v &
f /. w0 = f . w )
by A2, PARTFUN1:def 6;
then
f /. v0,
f /. w0 are_adjacent
by A2, CHORD:def 3;
then consider e being
object such that A3:
e Joins v0,
w0,
G1
by A1, A2, CHORD:def 3;
take e =
e;
e Joins v,w,G1thus
e Joins v,
w,
G1
by A3;
verum
end;
assume A4:
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
; f is continuous
let v, w be Vertex of G1; GLIB_011:def 3 ( v in dom f & w in dom f & f /. v,f /. w are_adjacent implies v,w are_adjacent )
assume A5:
( v in dom f & w in dom f )
; ( not f /. v,f /. w are_adjacent or v,w are_adjacent )
assume
f /. v,f /. w are_adjacent
; v,w are_adjacent
then consider e9 being object such that
A6:
e9 Joins f /. v,f /. w,G2
by CHORD:def 3;
( f /. v = f . v & f /. w = f . w )
by A5, PARTFUN1:def 6;
then consider e being object such that
A7:
e Joins v,w,G1
by A4, A5, A6;
thus
v,w are_adjacent
by A7, CHORD:def 3; verum