defpred S₁[ Element of NAT ] means for G being finite _Graph st G .size() = $1 holds
P₁[G];
A3: for k being Element of 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 Element of NAT holds S₁[k] from NAT_1:sch 1(A5, A3);
hence P₁[G] by A4; :: thesis: verum