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