let n be Nat; :: thesis: Seg n = (n + 1) \ {0}
A1: n + 1 = { m where m is Nat : m < n + 1 } by AXIOMS:4;
thus Seg n c= (n + 1) \ {0} :: according to XBOOLE_0:def 10 :: thesis: (n + 1) \ {0} c= Seg n
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Seg n or x in (n + 1) \ {0} )
assume x in Seg n ; :: thesis: x in (n + 1) \ {0}
then consider k being Nat such that
A2: x = k and
A3: 1 <= k and
A4: k <= n ;
k < n + 1 by A4, NAT_1:13;
then A5: x in n + 1 by A1, A2;
not x in {0} by A2, A3, TARSKI:def 1;
hence x in (n + 1) \ {0} by A5, XBOOLE_0:def 5; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (n + 1) \ {0} or x in Seg n )
assume A6: x in (n + 1) \ {0} ; :: thesis: x in Seg n
then A7: x in n + 1 ;
A8: not x in {0} by A6, XBOOLE_0:def 5;
consider m being Nat such that
A9: x = m and
A10: m < n + 1 by A1, A7;
A11: x <> 0 by A8, TARSKI:def 1;
0 + 1 = 1 ;
then A12: 1 <= m by A9, A11, NAT_1:13;
m <= n by A10, NAT_1:13;
hence x in Seg n by A9, A12; :: thesis: verum