for G being _finite _Graph holds P₁[G]

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