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:3;
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:3; :: 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