defpred S₁[ Element of NAT ] means { k where k is Element of NAT : k <= $1 } is finite ;
A1: { 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 A2: a in { k where k is Element of NAT : k <= 0 } ; :: thesis: a in {0 }
consider k being Element of NAT such that
A3: k = a and
A4: k <= 0 by A2;
A5: k = 0 by A4, NAT_1:3;
thus a in {0 } by A3, A5, 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 A6: a in {0 } ; :: thesis: a in { k where k is Element of NAT : k <= 0 }
A7: a = 0 by A6, TARSKI:def 1;
thus a in { k where k is Element of NAT : k <= 0 } by A7; :: thesis: verum

end;

end;

A8: S₁[ 0 ] by A1;
A9: 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 A10: S₁[n] ; :: thesis: S₁[n + 1]
A11: { l where l is Element of NAT : l <= n + 1 } = { k where k is Element of NAT : k <= n } \/ {(n + 1)} by Th11;
thus S₁[n + 1] by A10, A11; :: thesis: verum

end;

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