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

proof

assume {0} /\ {n} <> {} ; :: thesis: contradiction
then consider x being set 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;

then P1P: {0} misses {n} by XBOOLE_0:def 7;
P2: { k where k is Element of NAT : k <= n } = {0} \/ (Seg n)

proof

now :: thesis: for x being set st x in { k where k is Element of NAT : k <= n } holds
x in {0} \/ (Seg n)

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

end;

then A4: { k where k is Element of NAT : k <= n } c= {0} \/ (Seg n) by TARSKI:def 3;

now :: thesis: for x being set st x in {0} \/ (Seg n) holds
x in { k where k is Element of NAT : k <= n }

let x be set ; :: thesis: ( x in {0} \/ (Seg n) implies x in { k where k is Element of NAT : k <= n } )
assume A5: x in {0} \/ (Seg n) ; :: thesis: x in { k where k is Element of NAT : k <= n }
then reconsider m = x as Element of NAT ;
( m in {0} or m in Seg n ) by A5, 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 Element of NAT : k <= n } ; :: thesis: verum

end;

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

end;

thus n = (succ n) \ {n} by ORDINAL1:37
.= { k where k is Element of NAT : k <= n } \ {n} by NAT_1:54
.= ({0} \ {n}) \/ ((Seg n) \ {n}) by P2, XBOOLE_1:42
.= {0} \/ ((Seg n) \ {n}) by P1P, XBOOLE_1:83 ; :: thesis: verum