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

let F be PGraphMapping of G1,G2; :: thesis: ( F _V is one-to-one implies F is semi-continuous )
assume A1: F _V is one-to-one ; :: thesis:
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
set v1 = () . e;
set v2 = () . e;
A4: e Joins () . e,() . e,G1 by ;
A5: ( (the_Source_of G1) . e in dom (F _V) & () . e in dom (F _V) ) by ;
then (F _E) . e Joins (F _V) . (() . e),(F _V) . (() . e),G2 by A2, A4, Th4;
per cases ) . (() . e) = (F _V) . v & (F _V) . (() . e) = (F _V) . w ) or ( (F _V) . (() . e) = (F _V) . w & (F _V) . (() . e) = (F _V) . v ) ) by ;
suppose ( (F _V) . (() . e) = (F _V) . v & (F _V) . (() . e) = (F _V) . w ) ; :: thesis: e Joins v,w,G1
then ( (the_Source_of G1) . e = v & () . e = w ) by ;
hence e Joins v,w,G1 by A4; :: thesis: verum
end;
suppose ( (F _V) . (() . e) = (F _V) . w & (F _V) . (() . e) = (F _V) . v ) ; :: thesis: e Joins v,w,G1
then ( (the_Source_of G1) . e = w & () . e = v ) by ;
hence e Joins v,w,G1 by ; :: thesis: verum
end;
end;