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

A1: 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 consider i being Element of NAT such that
A2: ( e = i & 1 <= i & i <= n ) ;
thus e in Seg n by A2, FINSEQ_1:3; :: thesis: verum

end;

now

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

end;

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