let G1 be addEdge of G,v1,e,v2; :: thesis: 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 ) ; :: thesis: 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; :: thesis: ( u <> v implies u,v are_adjacent )
assume A2: u <> v ; :: thesis: 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; :: thesis: verum

end;

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

end;

suppose ( not v1 in the_Vertices_of G or not v2 in the_Vertices_of G or e in the_Edges_of G ) ; :: thesis: G1 is complete

then G1 == G by Def11;
hence G1 is complete by CHORD:62; :: thesis: verum

end;

end;