for G being _finite _Graph holds P₁[G]

A1: for G being _finite _Graph st G .order() = 1 holds
P₁[G] and
A2: for k being non zero Nat st ( for Gk being _finite _Graph st Gk .order() = k holds
P₁[Gk] ) holds
for Gk1 being _finite _Graph st Gk1 .order() = k + 1 holds
P₁[Gk1]