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