for G being _finite _Graph holds P₁[G]

A1: for G being _trivial edgeless _Graph holds P₁[G] and
A2: for G2 being _finite _Graph
for v being object
for G1 being addVertex of G2,v st not v in the_Vertices_of G2 & P₁[G2] holds
P₁[G1] and
A3: for G2 being _finite _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]