let G be finite _Graph; :: thesis: P_{1}[G]

defpred S_{1}[ non zero Nat] means for Gk being finite _Graph st Gk .order() < $1 holds

P_{1}[Gk];

A2: for n being non zero Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[1]
by NAT_1:14;

for k being non zero Nat holds S_{1}[k]
from NAT_1:sch 10(A4, A2);

then for Gk being finite _Graph st Gk .order() < G .order() holds

P_{1}[Gk]
;

hence P_{1}[G]
by A1; :: thesis: verum

defpred S

P

A2: for n being non zero Nat st S

S

proof

A4:
S
let n be non zero Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A3: S_{1}[n]
; :: thesis: S_{1}[n + 1]

_{1}[n + 1]
; :: thesis: verum

end;assume A3: S

now :: thesis: for Gk being finite _Graph st Gk .order() < n + 1 holds

P_{1}[Gk]

hence
SP

let Gk be finite _Graph; :: thesis: ( Gk .order() < n + 1 implies P_{1}[Gk] )

assume Gk .order() < n + 1 ; :: thesis: P_{1}[Gk]

then Gk .order() <= n by NAT_1:13;

then ( Gk .order() < n or Gk .order() = n ) by XXREAL_0:1;

hence P_{1}[Gk]
by A1, A3; :: thesis: verum

end;assume Gk .order() < n + 1 ; :: thesis: P

then Gk .order() <= n by NAT_1:13;

then ( Gk .order() < n or Gk .order() = n ) by XXREAL_0:1;

hence P

for k being non zero Nat holds S

then for Gk being finite _Graph st Gk .order() < G .order() holds

P

hence P