let G be _finite _Graph; :: thesis: P₁[G]
defpred S₁[ non zero Nat] means for Gk being _finite _Graph st Gk .order() < $1 holds
P₁[Gk];
A2: for n being non zero Nat st S₁[n] holds
S₁[n + 1]

proof

let n be non zero Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]

now :: thesis: for Gk being _finite _Graph st Gk .order() < n + 1 holds
P₁[Gk]

let Gk be _finite _Graph; :: thesis: ( Gk .order() < n + 1 implies P₁[Gk] )
assume Gk .order() < n + 1 ; :: thesis: P₁[Gk]
then Gk .order() <= n by NAT_1:13;
then ( Gk .order() < n or Gk .order() = n ) by XXREAL_0:1;
hence P₁[Gk] by A1, A3; :: thesis: verum

end;

hence S₁[n + 1] ; :: thesis: verum

end;

A4: S₁[1] by NAT_1:14;
for k being non zero Nat holds S₁[k] from NAT_1:sch 10(A4, A2);
then for Gk being _finite _Graph st Gk .order() < G .order() holds
P₁[Gk] ;
hence P₁[G] by A1; :: thesis: verum