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