let F be PGraphMapping of G1,G2; :: thesis: ( F is semi-continuous implies F is semi-Dcontinuous )
assume A4: F is semi-continuous ; :: thesis: 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 ; :: thesis: ( 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) ) ; :: thesis: ( 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 :: thesis: ( (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 implies e DJoins v,w,G1 )

assume e DJoins v,w,G1 ; :: thesis: (F _E) . e DJoins (F _V) . v,(F _V) . w,G2
then 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; :: thesis: verum

end;

assume (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 ; :: thesis: 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; :: thesis: verum

end;

hence F is semi-Dcontinuous ; :: thesis: verum