let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is strong_SG-embedding & G2 is complete holds
G1 is complete
let F be PGraphMapping of G1,G2; :: thesis: ( F is strong_SG-embedding & G2 is complete implies G1 is complete )
assume A1: F is strong_SG-embedding ; :: thesis: ( not G2 is complete or G1 is complete )
assume A2: G2 is complete ; :: thesis: G1 is complete

now :: thesis: for v, w being Vertex of G1 st v <> w holds
v,w are_adjacent

let v, w be Vertex of G1; :: thesis: ( v <> w implies v,w are_adjacent )
assume A3: v <> w ; :: thesis: v,w are_adjacent
( v in the_Vertices_of G1 & w in the_Vertices_of G1 ) ;
then A4: ( v in dom (F _V) & w in dom (F _V) ) by A1, Def11;
then ( (F _V) . v in rng (F _V) & (F _V) . w in rng (F _V) ) by FUNCT_1:3;
then reconsider v2 = (F _V) . v, w2 = (F _V) . w as Vertex of G2 ;
v2 <> w2 by A1, A3, A4, FUNCT_1:def 4;
then consider e2 being object such that
A5: e2 Joins v2,w2,G2 by A2, CHORD:def 6, CHORD:def 3;
consider e1 being object such that
A6: ( e1 Joins v,w,G1 & e1 in dom (F _E) & (F _E) . e1 = e2 ) by A1, A4, A5, Def16;
thus v,w are_adjacent by A6, CHORD:def 3; :: thesis: verum

end;

hence G1 is complete by CHORD:def 6; :: thesis: verum