let G2 be _Graph; 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; 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 ; 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; ( 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
; not G1 is complete
ex u, v being Vertex of G1 st
( u <> v & not u,v are_adjacent )
hence
not G1 is complete
by CHORD:def 6; verum