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 G2 is complete and
A2: v1,v2 are_adjacent ; :: thesis:

per cases ;

suppose A3: not e in the_Edges_of G2 ; :: thesis:

ex u1, u2 being Vertex of G1 st
( u1 <> u2 & not u1,u2 are_adjacent )

proof

consider u3, u4 being Vertex of G2 such that
A4: u3 <> u4 and
A5: not u3,u4 are_adjacent by A1, CHORD:def 6;
reconsider u1 = u3, u2 = u4 as Vertex of G1 by Th72;
take u1 ; :: thesis:
take u2 ; :: thesis:
thus u1 <> u2 by A4; :: thesis:
for e1 being object holds not e1 Joins u1,u2,G1

proof

given e1 being object such that A6: e1 Joins u1,u2,G1 ; :: thesis:

per cases by A6, Th76;

suppose e1 Joins u1,u2,G2 ; :: thesis:

hence contradiction by A5, CHORD:def 3; :: thesis:

end;

suppose A7: not e1 in the_Edges_of G2 ; :: thesis:

A8: e1 in the_Edges_of G1 by A6, GLIB_000:def 13;
the_Edges_of G1 = (the_Edges_of G2) \/ {e} by A3, Def11;
then e1 in {e} by A7, A8, XBOOLE_0:def 3;
then e1 = e by TARSKI:def 1;
then e1 DJoins v1,v2,G1 by A7, Th109;
then e1 Joins v1,v2,G1 by GLIB_000:16;

per cases by A6, GLIB_000:15;

suppose ( v1 = u1 & v2 = u2 ) ; :: thesis:

hence contradiction by A2, A5; :: thesis:

end;

suppose ( v1 = u2 & v2 = u1 ) ; :: thesis:

hence contradiction by A2, A5; :: thesis:

end;

end;

end;

end;

end;

hence not u1,u2 are_adjacent by CHORD:def 3; :: thesis:

end;

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

end;

suppose e in the_Edges_of G2 ; :: thesis:

then G1 == G2 by Def11;
hence not G1 is complete by A1, CHORD:62; :: thesis:

end;

end;