for G being _finite connected _Graph holds P₁[G]

A1: for G being _trivial edgeless _Graph holds P₁[G] and
A2: for G2 being _finite connected _Graph
for v being Vertex of G2
for e, w being object st not e in the_Edges_of G2 & not w in the_Vertices_of G2 & P₁[G2] holds
( ( for G1 being addAdjVertex of G2,v,e,w holds P₁[G1] ) & ( for G1 being addAdjVertex of G2,w,e,v holds P₁[G1] ) ) and
A3: for G2 being _finite connected _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 & P₁[G2] holds
P₁[G1]