set r = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } ;
{ [i,(i + 1)] where i is Element of NAT : i + 1 < n } c= [:n,n:]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } or x in [:n,n:] )
assume x in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } ; :: thesis: x in [:n,n:]
then consider i being Element of NAT such that
A1: x = [i,(i + 1)] and
A2: i + 1 < n ;
i <= i + 1 by NAT_1:11;
then i < n by A2, XXREAL_0:2;
then ( i in n & i + 1 in n ) by A2, NAT_1:45;
hence x in [:n,n:] by A1, ZFMISC_1:106; :: thesis: verum

end;

then reconsider r = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } as Relation of n ;
take RelStr(# n,r #) ; :: thesis: ( the carrier of RelStr(# n,r #) = n & the InternalRel of RelStr(# n,r #) = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } )
thus ( the carrier of RelStr(# n,r #) = n & the InternalRel of RelStr(# n,r #) = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } ) ; :: thesis: verum