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;