let n be natural number ; :: thesis: succ n = n + 1
A1: n + 1 = { L where L is Element of NAT : L < n + 1 } by AXIOMS:4;
A2: n = { K where K is Element of NAT : K < n } by AXIOMS:4;
thus succ n c= n + 1 :: according to XBOOLE_0:def 10 :: thesis: n + 1 c= succ n

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in succ n or x in n + 1 )
assume A3: x in succ n ; :: thesis: x in n + 1

per cases ( x in n or x = n ) by A3, ORDINAL1:8;

suppose x in n ; :: thesis: x in n + 1

then consider K being Element of NAT such that
A4: x = K and
A5: K < n by A2;
K < n + 1 by A5, Th13;
hence x in n + 1 by A1, A4; :: thesis: verum

end;

suppose A6: x = n ; :: thesis: x in n + 1

reconsider n = n as Element of NAT by ORDINAL1:def 12;
n < n + 1 by Th13;
hence x in n + 1 by A1, A6; :: thesis: verum

end;

end;

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in n + 1 or x in succ n )
assume x in n + 1 ; :: thesis: x in succ n
then consider K being Element of NAT such that
A7: x = K and
A8: K < n + 1 by A1;
K <= n by A8, Th13;
then ( K = n or K < n ) by XXREAL_0:1;
then ( x = n or x in n ) by A2, A7;
hence x in succ n by ORDINAL1:8; :: thesis: verum