let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is Dcontinuous & F is strong_SG-embedding & G2 is Dcomplete holds
G1 is Dcomplete
let F be PGraphMapping of G1,G2; :: thesis: ( F is Dcontinuous & F is strong_SG-embedding & G2 is Dcomplete implies G1 is Dcomplete )
assume A1: ( F is Dcontinuous & F is strong_SG-embedding & G2 is Dcomplete ) ; :: thesis: G1 is Dcomplete
let v, w be Vertex of G1; :: according to GLIB_016:def 1 :: thesis: ( v <> w implies ex e being object st e DJoins v,w,G1 )
assume A2: v <> w ; :: thesis: ex e being object st e DJoins v,w,G1
dom (F _V) = the_Vertices_of G1 by A1, GLIB_010:def 11;
then A3: ( v in dom (F _V) & w in dom (F _V) ) ;
then A4: ( (F _V) . v = (F _V) /. v & (F _V) . w = (F _V) /. w ) by PARTFUN1:def 6;
then (F _V) /. v <> (F _V) /. w by A1, A2, A3, FUNCT_1:def 4;
then consider e9 being object such that
A5: e9 DJoins (F _V) /. v,(F _V) /. w,G2 by A1;
e9 DJoins (F _V) . v,(F _V) . w,G2 by A4, A5;
then consider e being object such that
A6: ( e DJoins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) by A1, A3, GLIB_010:def 18;
take e ; :: thesis: e DJoins v,w,G1
thus e DJoins v,w,G1 by A6; :: thesis: verum