let n be natural number ; :: thesis: succ n = n + 1
A1: ( n = { K where K is Element of NAT : K < n } & n + 1 = { L where L is Element of NAT : L < n + 1 } ) by AXIOMS:30;
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 A2: x in succ n ; :: thesis: x in n + 1

per cases ( x in n or x = n ) by A2, ORDINAL1:13;

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

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

end;

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

reconsider n = n as Element of NAT by ORDINAL1:def 13;
n < n + 1 by Th13;
hence x in n + 1 by A1, A5; :: 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
A6: ( x = K & K < n + 1 ) by A1;
K <= n by A6, Th13;
then ( K = n or K < n ) by XXREAL_0:1;
then ( x = n or x in n ) by A1, A6;
hence x in succ n by ORDINAL1:13; :: thesis: verum