defpred S₁[ Element of NAT ] means { k where k is Element of NAT : k <= $1 } is finite ;
{ k where k is Element of NAT : k <= 0 } = {0}

proof

thus { k where k is Element of NAT : k <= 0 } c= {0} :: according to XBOOLE_0:def 10 :: thesis: {0} c= { k where k is Element of NAT : k <= 0 }

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { k where k is Element of NAT : k <= 0 } or a in {0} )
assume a in { k where k is Element of NAT : k <= 0 } ; :: thesis: a in {0}
then consider k being Element of NAT such that
A1: k = a and
A2: k <= 0 ;
k = 0 by A2, NAT_1:3;
hence a in {0} by A1, TARSKI:def 1; :: thesis: verum

end;

thus {0} c= { k where k is Element of NAT : k <= 0 } :: thesis: verum

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in {0} or a in { k where k is Element of NAT : k <= 0 } )
assume a in {0} ; :: thesis: a in { k where k is Element of NAT : k <= 0 }
then a = 0 by TARSKI:def 1;
hence a in { k where k is Element of NAT : k <= 0 } ; :: thesis: verum

end;

end;

then A3: S₁[ 0 ] ;
A4: 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 A5: S₁[n] ; :: thesis: S₁[n + 1]
{ l where l is Element of NAT : l <= n + 1 } = { k where k is Element of NAT : k <= n } \/ {(n + 1)} by Th11;
hence S₁[n + 1] by A5; :: thesis: verum

end;

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