let n be non zero Nat; :: thesis: n = {0} \/ ((Seg n) \ {n})
A1: {0} /\ {n} = {}

proof

assume {0} /\ {n} <> {} ; :: thesis: contradiction
then consider x being object such that
A2: x in {0} /\ {n} by XBOOLE_0:def 1;
( x in {0} & x in {n} ) by A2, XBOOLE_0:def 4;
then ( x = 0 & x = n ) by TARSKI:def 1;
hence contradiction ; :: thesis: verum

end;

A3: { k where k is Nat : k <= n } = {0} \/ (Seg n)

proof

now :: thesis: for x being object st x in { k where k is Nat : k <= n } holds
x in {0} \/ (Seg n)

let x be object ; :: thesis: ( x in { k where k is Nat : k <= n } implies x in {0} \/ (Seg n) )
assume x in { k where k is Nat : k <= n } ; :: thesis: x in {0} \/ (Seg n)
then consider m being Nat such that
A4: ( m = x & m <= n ) ;
( m = 0 or ( 1 <= m & m <= n ) ) by A4, NAT_1:14;
then ( m in {0} or m in Seg n ) by TARSKI:def 1;
hence x in {0} \/ (Seg n) by A4, XBOOLE_0:def 3; :: thesis: verum

end;

then A5: { k where k is Nat : k <= n } c= {0} \/ (Seg n) by TARSKI:def 3;

now :: thesis: for x being object st x in {0} \/ (Seg n) holds
x in { k where k is Nat : k <= n }

let x be object ; :: thesis: ( x in {0} \/ (Seg n) implies x in { k where k is Nat : k <= n } )
assume A6: x in {0} \/ (Seg n) ; :: thesis: x in { k where k is Nat : k <= n }
then reconsider m = x as Element of NAT ;
( m in {0} or m in Seg n ) by A6, XBOOLE_0:def 3;
then ( m = 0 or ( 1 <= m & m <= n ) ) by FINSEQ_1:1, TARSKI:def 1;
hence x in { k where k is Nat : k <= n } ; :: thesis: verum

end;

then {0} \/ (Seg n) c= { k where k is Nat : k <= n } by TARSKI:def 3;
hence { k where k is Nat : k <= n } = {0} \/ (Seg n) by A5, XBOOLE_0:def 10; :: thesis: verum

end;

thus n = (succ (Segm n)) \ {n} by ORDINAL1:37
.= { k where k is Nat : k <= n } \ {n} by NAT_1:54
.= ({0} \ {n}) \/ ((Seg n) \ {n}) by A3, XBOOLE_1:42
.= {0} \/ ((Seg n) \ {n}) by A1, XBOOLE_0:def 7, XBOOLE_1:83 ; :: thesis: verum