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

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

hence
G1 is complete
by CHORD:def 6; :: thesis: verumv,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;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