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