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 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 ;
then A3: i in Segm n by NAT_1:44;
i + 1 in Segm n by ;
hence x in [:n,n:] by ; :: 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