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 ;
TARSKI:def 3 ( 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 }
;
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;
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 #)
; ( 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 } )
; verum