defpred S₁[ Nat] means for G being finite _Graph st G .order() = $1 holds
P₁[G];
A3: for k being non empty Nat st S₁[k] holds
S₁[k + 1] by A2;
let G be finite _Graph; :: thesis: P₁[G]
A4: G .order() = G .order() ;
A5: S₁[1] by A1;
for k being non empty Nat holds S₁[k] from NAT_1:sch 10(A5, A3);
hence P₁[G] by A4; :: thesis: verum