let F be PGraphMapping of G1,G2; :: thesis: ( F is semi-Dcontinuous implies ( F is directed & F is semi-continuous ) )

assume A1: F is semi-Dcontinuous ; :: thesis: ( F is directed & F is semi-continuous )

hence F is directed by Th16; :: thesis: F is semi-continuous

let e, v, w be object ; :: according to GLIB_010:def 15 :: thesis: ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & (F _E) . e Joins (F _V) . v,(F _V) . w,G2 implies e Joins v,w,G1 )

assume A2: ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) ) ; :: thesis: ( not (F _E) . e Joins (F _V) . v,(F _V) . w,G2 or e Joins v,w,G1 )

assume (F _E) . e Joins (F _V) . v,(F _V) . w,G2 ; :: thesis: e Joins v,w,G1

assume A1: F is semi-Dcontinuous ; :: thesis: ( F is directed & F is semi-continuous )

hence F is directed by Th16; :: thesis: F is semi-continuous

let e, v, w be object ; :: according to GLIB_010:def 15 :: thesis: ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & (F _E) . e Joins (F _V) . v,(F _V) . w,G2 implies e Joins v,w,G1 )

assume A2: ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) ) ; :: thesis: ( not (F _E) . e Joins (F _V) . v,(F _V) . w,G2 or e Joins v,w,G1 )

assume (F _E) . e Joins (F _V) . v,(F _V) . w,G2 ; :: thesis: e Joins v,w,G1