let F be PGraphMapping of G1,G2; :: thesis: ( F is Dcontinuous implies F is continuous )
assume A3: F is Dcontinuous ; :: thesis: F is continuous
let e9, v, w be object ; :: according to GLIB_010:def 16 :: thesis: ( v in dom (F _V) & w in dom (F _V) & e9 Joins (F _V) . v,(F _V) . w,G2 implies ex e being object st
( e Joins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) )
assume A4: ( v in dom (F _V) & w in dom (F _V) & e9 Joins (F _V) . v,(F _V) . w,G2 ) ; :: thesis: ex e being object st
( e Joins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 )

per cases then ( e9 DJoins (F _V) . v,(F _V) . w,G2 or e9 DJoins (F _V) . w,(F _V) . v,G2 ) by GLIB_000:16;

suppose e9 DJoins (F _V) . v,(F _V) . w,G2 ; :: thesis: ex e being object st
( e Joins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 )

then consider e being object such that
A5: ( e DJoins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) by A3, A4;
take e ; :: thesis: ( e Joins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 )
thus ( e Joins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) by A5, GLIB_000:16; :: thesis: verum

end;

suppose e9 DJoins (F _V) . w,(F _V) . v,G2 ; :: thesis: ex e being object st
( e Joins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 )

then consider e being object such that
A6: ( e DJoins w,v,G1 & e in dom (F _E) & (F _E) . e = e9 ) by A3, A4;
take e ; :: thesis: ( e Joins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 )
thus ( e Joins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) by A6, GLIB_000:16; :: thesis: verum

end;

end;