let G2 be _Graph; for v1, e being object
for v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2 st not v1 in the_Vertices_of G2 & not e in the_Edges_of G2 holds
not G1 is _trivial
let v1, e be object ; for v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2 st not v1 in the_Vertices_of G2 & not e in the_Edges_of G2 holds
not G1 is _trivial
let v2 be Vertex of G2; for G1 being addAdjVertex of G2,v1,e,v2 st not v1 in the_Vertices_of G2 & not e in the_Edges_of G2 holds
not G1 is _trivial
let G1 be addAdjVertex of G2,v1,e,v2; ( not v1 in the_Vertices_of G2 & not e in the_Edges_of G2 implies not G1 is _trivial )
assume A1:
( not v1 in the_Vertices_of G2 & not e in the_Edges_of G2 )
; not G1 is _trivial
then consider G3 being addVertex of G2,v1 such that
A2:
G1 is addEdge of G3,v1,e,v2
by Th130;
{v1} \ (the_Vertices_of G2) <> {}
by A1, ZFMISC_1:59;
then
not G3 is _trivial
by Th93;
hence
not G1 is _trivial
by A2; verum