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: ({1} \/ { k where k is Element of NAT : ( 1 < k & k < n ) } ) \/ {n} c= Seg n

proof

let d be object ; :: 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 )
A3: { k where k is Element of NAT : ( 1 < k & k < n ) } c= Seg n

proof

let d be object ; :: according to TARSKI:def 3 :: thesis: ( not d in { k where k is Element of NAT : ( 1 < k & k < n ) } or d in Seg n )
assume d in { k where k is Element of NAT : ( 1 < k & k < n ) } ; :: thesis: d in Seg n
then ex k being Element of NAT st
( d = k & 1 < k & k < n ) ;
hence d in Seg n ; :: thesis: verum

end;

1 in Seg n by A1;
then {1} c= Seg n by ZFMISC_1:31;
then A4: {1} \/ { k where k is Element of NAT : ( 1 < k & k < n ) } c= Seg n by A3, XBOOLE_1:8;
n in Seg n by A1;
then {n} c= Seg n by ZFMISC_1:31;
then ({1} \/ { k where k is Element of NAT : ( 1 < k & k < n ) } ) \/ {n} c= Seg n by A4, XBOOLE_1:8;
hence ( not d in ({1} \/ { k where k is Element of NAT : ( 1 < k & k < n ) } ) \/ {n} or d in Seg n ) ; :: thesis: verum

end;

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

proof

let d be object ; :: 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 A5: 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 A6: 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 A5;
A7: l <= n by A5, FINSEQ_1:1;
1 <= l by A5, FINSEQ_1:1;
then ( 1 = l or ( 1 < l & l < n ) or l = n or 1 = n ) by A7, 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 A6, 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 A5, FINSEQ_1:2, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

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