let G1 be addEdge of G,v1,e,v2; G1 is complete
per cases
( ( v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G ) or not v1 in the_Vertices_of G or not v2 in the_Vertices_of G or e in the_Edges_of G )
;
suppose A1:
(
v1 in the_Vertices_of G &
v2 in the_Vertices_of G & not
e in the_Edges_of G )
;
G1 is complete
for
u,
v being
Vertex of
G1 st
u <> v holds
u,
v are_adjacent
proof
let u,
v be
Vertex of
G1;
( u <> v implies u,v are_adjacent )
assume A2:
u <> v
;
u,v are_adjacent
reconsider u1 =
u,
v1 =
v as
Vertex of
G by A1, Def11;
consider e1 being
object such that A3:
e1 Joins u1,
v1,
G
by A2, CHORD:def 6, CHORD:def 3;
reconsider u1 =
u1,
v1 =
v1 as
set ;
thus
u,
v are_adjacent
by A3, Th74, CHORD:def 3;
verum
end; hence
G1 is
complete
by CHORD:def 6;
verum