let UN be Universe; :: thesis: for n being Nat holds n in UN
defpred S₁[ Nat] means $1 in UN;
A1: S₁[ 0 ] by Th13;

now :: thesis: for n being Nat st S₁[n] holds
n + 1 in UN

let n be Nat; :: thesis: ( S₁[n] implies n + 1 in UN )
assume A2: S₁[n] ; :: thesis: n + 1 in UN
A3: n (+) 1 = succ n by ORDINAL7:77;
reconsider n9 = n as Element of UN by A2;
succ n9 in UN ;
hence n + 1 in UN by A3, ORDINAL7:76; :: thesis: verum

end;

then A4: for n being Nat st S₁[n] holds
S₁[n + 1] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A4);
hence for n being Nat holds n in UN ; :: thesis: verum