let F be PGraphMapping of G1,G2; ( F is semi-continuous implies F is semi-Dcontinuous )
assume A4:
F is semi-continuous
; F is semi-Dcontinuous
consider u being Vertex of G1 such that
A5:
the_Vertices_of G1 = {u}
by GLIB_000:22;
for e, v, w being object st e in dom (F _E) & v in dom (F _V) & w in dom (F _V) holds
( e DJoins v,w,G1 iff (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 )
proof
let e,
v,
w be
object ;
( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) implies ( e DJoins v,w,G1 iff (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 ) )
assume A6:
(
e in dom (F _E) &
v in dom (F _V) &
w in dom (F _V) )
;
( e DJoins v,w,G1 iff (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 )
then A7:
(
v = u &
w = u )
by A5, TARSKI:def 1;
hereby ( (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 implies e DJoins v,w,G1 )
assume
e DJoins v,
w,
G1
;
(F _E) . e DJoins (F _V) . v,(F _V) . w,G2then
e Joins u,
u,
G1
by A7, GLIB_000:16;
hence
(F _E) . e DJoins (F _V) . v,
(F _V) . w,
G2
by A6, A7, Th4, GLIB_000:16;
verum
end;
assume
(F _E) . e DJoins (F _V) . v,
(F _V) . w,
G2
;
e DJoins v,w,G1
then
(F _E) . e Joins (F _V) . u,
(F _V) . u,
G2
by A7, GLIB_000:16;
then
e Joins u,
u,
G1
by A4, A6, A7;
hence
e DJoins v,
w,
G1
by A7, GLIB_000:16;
verum
end;
hence
F is semi-Dcontinuous
; verum