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:]

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

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

proof

then reconsider r = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } as Relation of n ;
let x be object ; :: 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 A3: i in Segm n by NAT_1:44;

i + 1 in Segm n by A2, NAT_1:44;

hence x in [:n,n:] by A1, A3, ZFMISC_1:87; :: thesis: verum

end;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 A3: i in Segm n by NAT_1:44;

i + 1 in Segm n by A2, NAT_1:44;

hence x in [:n,n:] by A1, A3, ZFMISC_1:87; :: thesis: verum

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