let n be Element of NAT ; :: thesis: nat_interval (1,n) = Seg n

now

let e be set ; :: thesis: ( e in Seg n implies e in nat_interval (1,n) )
assume A1: e in Seg n ; :: thesis: e in nat_interval (1,n)
then reconsider i = e as Element of NAT ;
( 1 <= i & i <= n ) by A1, FINSEQ_1:1;
hence e in nat_interval (1,n) ; :: thesis: verum

end;

then A2: Seg n c= nat_interval (1,n) by TARSKI:def 3;

now

let e be set ; :: thesis: ( e in nat_interval (1,n) implies e in Seg n )
assume e in nat_interval (1,n) ; :: thesis: e in Seg n
then ex i being Element of NAT st
( e = i & 1 <= i & i <= n ) ;
hence e in Seg n by FINSEQ_1:1; :: thesis: verum

end;

then nat_interval (1,n) c= Seg n by TARSKI:def 3;
hence nat_interval (1,n) = Seg n by A2, XBOOLE_0:def 10; :: thesis: verum