let G2 be _Graph; :: thesis: for v1 being Vertex of G2
for e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 & not G2 is _trivial holds
not G1 is complete
let v1 be Vertex of G2; :: thesis: for e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 & not G2 is _trivial holds
not G1 is complete
let e, v2 be object ; :: thesis: for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 & not G2 is _trivial holds
not G1 is complete
let G1 be addAdjVertex of G2,v1,e,v2; :: thesis: ( not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 & not G2 is _trivial implies not G1 is complete )
assume that
A1: ( not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 ) and
A2: not G2 is _trivial ; :: thesis: not G1 is complete
ex u, v being Vertex of G1 st
( u <> v & not u,v are_adjacent )

proof

consider u1, u2 being Vertex of G2 such that
A3: u1 <> u2 by A2, GLIB_000:21;
A4: ( u1 <> v2 & u2 <> v2 ) by A1;
reconsider u1 = u1, u2 = u2 as Vertex of G1 by Th72;
reconsider v2 = v2 as Vertex of G1 by A1, Th133;

per cases ( u1 <> v1 or u2 <> v1 or ( u1 = v1 & u2 = v1 ) ) ;

suppose A5: u1 <> v1 ; :: thesis: ex u, v being Vertex of G1 st
( u <> v & not u,v are_adjacent )

take u1 ; :: thesis: ex v being Vertex of G1 st
( u1 <> v & not u1,v are_adjacent )
take v2 ; :: thesis: ( u1 <> v2 & not u1,v2 are_adjacent )
for e1 being object holds not e1 Joins u1,v2,G1 by A1, A5, Th137;
hence ( u1 <> v2 & not u1,v2 are_adjacent ) by A4, CHORD:def 3; :: thesis: verum

end;

suppose A6: u2 <> v1 ; :: thesis: ex u, v being Vertex of G1 st
( u <> v & not u,v are_adjacent )

take u2 ; :: thesis: ex v being Vertex of G1 st
( u2 <> v & not u2,v are_adjacent )
take v2 ; :: thesis: ( u2 <> v2 & not u2,v2 are_adjacent )
for e1 being object holds not e1 Joins u2,v2,G1 by A1, A6, Th137;
hence ( u2 <> v2 & not u2,v2 are_adjacent ) by A4, CHORD:def 3; :: thesis: verum

end;

suppose ( u1 = v1 & u2 = v1 ) ; :: thesis: ex u, v being Vertex of G1 st
( u <> v & not u,v are_adjacent )

hence ex u, v being Vertex of G1 st
( u <> v & not u,v are_adjacent ) by A3; :: thesis: verum

end;

end;

end;

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