scheme :: GLIB_008:sch 6
FinSimpleConnectedGraphs{ P₁[ _finite _Graph] } :

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

provided

A1: for G being _trivial edgeless _Graph holds P₁[G] and
A2: for G2 being _finite simple connected _Graph
for v being object
for V being non empty finite set
for G1 being addAdjVertexAll of G2,v,V st not v in the_Vertices_of G2 & V c= the_Vertices_of G2 & P₁[G2] holds
P₁[G1]