scheme :: CHORD:sch 1
FinGraphOrderCompInd{ P1[ set ] } :
for G being _finite _Graph holds P1[G]
provided
A1: for k being non zero Nat st ( for Gk being _finite _Graph st Gk .order() < k holds
P1[Gk] ) holds
for Gk1 being _finite _Graph st Gk1 .order() = k holds
P1[Gk1]