let G1 be addAdjVertex of G,v1,e,v2; :: thesis: not G1 is complete
A1: not G is _trivial ;

per cases ( ( v1 in the_Vertices_of G & not e in the_Edges_of G & not v2 in the_Vertices_of G ) or ( not v1 in the_Vertices_of G & not e in the_Edges_of G & v2 in the_Vertices_of G ) or ( ( not v1 in the_Vertices_of G or e in the_Edges_of G or v2 in the_Vertices_of G ) & ( v1 in the_Vertices_of G or e in the_Edges_of G or not v2 in the_Vertices_of G ) ) ) ;

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

hence not G1 is complete by A1, Th152; :: thesis: verum

end;

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

hence not G1 is complete by A1, Th153; :: thesis: verum

end;

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

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

end;

end;