let n be Nat; :: thesis: ( n >= 1 implies Seg n = ({1} \/ { k where k is Element of NAT : ( 1 < k & k < n ) } ) \/ {n} )
assume A1: n >= 1 ; :: thesis: Seg n = ({1} \/ { k where k is Element of NAT : ( 1 < k & k < n ) } ) \/ {n}
A2: n in NAT by ORDINAL1:def 13;
A3: Seg n c= ({1} \/ { k where k is Element of NAT : ( 1 < k & k < n ) } ) \/ {n}

proof

let d be set ; :: according to TARSKI:def 3 :: thesis: ( not d in Seg n or d in ({1} \/ { k where k is Element of NAT : ( 1 < k & k < n ) } ) \/ {n} )
assume A4: d in Seg n ; :: thesis: d in ({1} \/ { k where k is Element of NAT : ( 1 < k & k < n ) } ) \/ {n}

per cases ( n > 1 or n = 1 ) by A1, XXREAL_0:1;

suppose A5: n > 1 ; :: thesis: d in ({1} \/ { k where k is Element of NAT : ( 1 < k & k < n ) } ) \/ {n}

reconsider l = d as Element of NAT by A4;
( 1 <= l & l <= n ) by A4, FINSEQ_1:3;
then ( 1 = l or ( 1 < l & l < n ) or l = n or 1 = n ) by XXREAL_0:1;
then ( d in {1} or d in { k where k is Element of NAT : ( 1 < k & k < n ) } or d in {n} ) by A5, TARSKI:def 1;
then ( d in {1} \/ { k where k is Element of NAT : ( 1 < k & k < n ) } or d in {n} ) by XBOOLE_0:def 3;
hence d in ({1} \/ { k where k is Element of NAT : ( 1 < k & k < n ) } ) \/ {n} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose n = 1 ; :: thesis: d in ({1} \/ { k where k is Element of NAT : ( 1 < k & k < n ) } ) \/ {n}

hence d in ({1} \/ { k where k is Element of NAT : ( 1 < k & k < n ) } ) \/ {n} by A4, FINSEQ_1:4, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

({1} \/ { k where k is Element of NAT : ( 1 < k & k < n ) } ) \/ {n} c= Seg n

proof

A6: for d being set st d in {1} holds
d in Seg n

proof

let d be set ; :: thesis: ( d in {1} implies d in Seg n )
assume d in {1} ; :: thesis: d in Seg n
then d = 1 by TARSKI:def 1;
hence d in Seg n by A1; :: thesis: verum

end;

A7: for d being set st d in { k where k is Element of NAT : ( 1 < k & k < n ) } holds
d in Seg n

proof

let d be set ; :: thesis: ( d in { k where k is Element of NAT : ( 1 < k & k < n ) } implies d in Seg n )
assume d in { k where k is Element of NAT : ( 1 < k & k < n ) } ; :: thesis: d in Seg n
then consider k being Element of NAT such that
A8: ( d = k & 1 < k & k < n ) ;
thus d in Seg n by A8; :: thesis: verum

end;

A9: for d being set st d in {n} holds
d in Seg n

proof

let d be set ; :: thesis: ( d in {n} implies d in Seg n )
assume d in {n} ; :: thesis: d in Seg n
then d = n by TARSKI:def 1;
hence d in Seg n by A1, A2; :: thesis: verum

end;

let d be set ; :: according to TARSKI:def 3 :: thesis: ( not d in ({1} \/ { k where k is Element of NAT : ( 1 < k & k < n ) } ) \/ {n} or d in Seg n )
assume d in ({1} \/ { k where k is Element of NAT : ( 1 < k & k < n ) } ) \/ {n} ; :: thesis: d in Seg n
then ( d in {1} \/ { k where k is Element of NAT : ( 1 < k & k < n ) } or d in {n} ) by XBOOLE_0:def 3;
then ( d in {1} or d in { k where k is Element of NAT : ( 1 < k & k < n ) } or d in {n} ) by XBOOLE_0:def 3;
hence d in Seg n by A6, A7, A9; :: thesis: verum

end;

hence Seg n = ({1} \/ { k where k is Element of NAT : ( 1 < k & k < n ) } ) \/ {n} by A3, XBOOLE_0:def 10; :: thesis: verum