let G1, G2 be _Graph; :: thesis: for F being continuous PGraphMapping of G1,G2 st F _E is one-to-one holds

F is semi-continuous

let F be continuous PGraphMapping of G1,G2; :: thesis: ( F _E is one-to-one implies F is semi-continuous )

assume A1: F _E is one-to-one ; :: 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 that

A2: ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) ) and

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

consider e0 being object such that

A4: ( e0 Joins v,w,G1 & e0 in dom (F _E) & (F _E) . e0 = (F _E) . e ) by A2, A3, Def16;

thus e Joins v,w,G1 by A1, A2, A4, FUNCT_1:def 4; :: thesis: verum

F is semi-continuous

let F be continuous PGraphMapping of G1,G2; :: thesis: ( F _E is one-to-one implies F is semi-continuous )

assume A1: F _E is one-to-one ; :: 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 that

A2: ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) ) and

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

consider e0 being object such that

A4: ( e0 Joins v,w,G1 & e0 in dom (F _E) & (F _E) . e0 = (F _E) . e ) by A2, A3, Def16;

thus e Joins v,w,G1 by A1, A2, A4, FUNCT_1:def 4; :: thesis: verum