let G2 be _Graph; :: thesis:
let v1, v2 be Vertex of G2; :: thesis:
let e be object ; :: thesis:
let G1 be addEdge of G2,v1,e,v2; :: thesis:
assume that
A1: not e in the_Edges_of G2 and
A2: for v3, v4 being Vertex of G2 holds
( v3,v4 are_adjacent or v3 = v4 or ( v1 = v3 & v2 = v4 ) or ( v1 = v4 & v2 = v3 ) ) ; :: thesis:
for u1, u2 being Vertex of G1 st u1 <> u2 holds
u1,u2 are_adjacent

proof

let u1, u2 be Vertex of G1; :: thesis:
assume A3: u1 <> u2 ; :: thesis:
reconsider u3 = u1, u4 = u2 as Vertex of G2 by Th108;

per cases ;

suppose u3,u4 are_adjacent ; :: thesis:

then consider e1 being object such that
A4: e1 Joins u3,u4,G2 by CHORD:def 3;
thus u1,u2 are_adjacent by A4, Th74, CHORD:def 3; :: thesis:

end;

suppose not u3,u4 are_adjacent ; :: thesis:

per cases by A2;

suppose u3 = u4 ; :: thesis:

hence u1,u2 are_adjacent by A3; :: thesis:

end;

suppose ( v1 = u3 & v2 = u4 ) ; :: thesis:

then e DJoins u1,u2,G1 by A1, Th109;
then e Joins u1,u2,G1 by GLIB_000:16;
hence u1,u2 are_adjacent by CHORD:def 3; :: thesis:

end;

suppose ( v1 = u4 & v2 = u3 ) ; :: thesis:

then e DJoins u2,u1,G1 by A1, Th109;
then e Joins u1,u2,G1 by GLIB_000:16;
hence u1,u2 are_adjacent by CHORD:def 3; :: thesis:

end;

end;

end;

end;

end;

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