let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 holds
( F is semi-Dcontinuous iff 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 ) )
let F be PGraphMapping of G1,G2; :: thesis: ( F is semi-Dcontinuous iff 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 ) )
thus ( F is semi-Dcontinuous implies 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 ) ) :: thesis: ( ( 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 ) ) implies F is semi-Dcontinuous )

proof

assume A1: F is semi-Dcontinuous ; :: thesis: 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 )
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 A2: ( 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 )
thus ( e DJoins v,w,G1 implies (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 ) :: thesis: ( (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 implies e DJoins v,w,G1 )

proof

assume A3: e DJoins v,w,G1 ; :: thesis: (F _E) . e DJoins (F _V) . v,(F _V) . w,G2
then e Joins v,w,G1 by GLIB_000:16;
then A4: (F _E) . e Joins (F _V) . v,(F _V) . w,G2 by A2, Th4;
assume A5: not (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 ; :: thesis: contradiction
then A6: (F _E) . e DJoins (F _V) . w,(F _V) . v,G2 by A4, GLIB_000:16;
then e DJoins w,v,G1 by A1, A2;
then ( (the_Source_of G1) . e = w & (the_Target_of G1) . e = v ) by GLIB_000:def 14;
then v = w by A3, GLIB_000:def 14;
hence contradiction by A5, A6; :: thesis: verum

end;

thus ( (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 implies e DJoins v,w,G1 ) by A1, A2; :: thesis: verum

end;

thus ( ( 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 ) ) implies F is semi-Dcontinuous ) ; :: thesis: verum