defpred S₁[ Element of NAT ] means $1 is finite ;
A1: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then succ n is finite ;
hence S₁[n + 1] by NAT_1:39; :: thesis: verum

end;

A2: S₁[ 0 ] ;
thus for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A1); :: thesis: verum