let n be Nat; :: thesis: the InternalRel of (Necklace n) = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } \/ { [(i + 1),i] where i is Element of NAT : i + 1 < n }

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

{ [i,(i + 1)] where i is Element of NAT : i + 1 < n } is Relation-like

set B = n -SuccRelStr ;

deffunc H_{1}( Element of NAT ) -> Element of NAT = $1;

deffunc H_{2}( Element of NAT ) -> Element of omega = $1 + 1;

defpred S_{1}[ Element of NAT ] means $1 + 1 < n;

set R = { [H_{2}(i),H_{1}(i)] where i is Element of NAT : S_{1}[i] } ;

A1: I = { [H_{1}(i),H_{2}(i)] where i is Element of NAT : S_{1}[i] }
;

A2: I ~ = { [H_{2}(i),H_{1}(i)] where i is Element of NAT : S_{1}[i] }
from NECKLACE:sch 1(A1);

the InternalRel of (n -SuccRelStr) = I by Def6;

hence the InternalRel of (Necklace n) = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } \/ { [(i + 1),i] where i is Element of NAT : i + 1 < n } by A2, Def7; :: thesis: verum

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

{ [i,(i + 1)] where i is Element of NAT : i + 1 < n } is Relation-like

proof

then reconsider I = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } as Relation ;
let x be object ; :: according to RELAT_1:def 1 :: thesis: ( not x in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } or ex b_{1}, b_{2} being object st x = [b_{1},b_{2}] )

assume x in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } ; :: thesis: ex b_{1}, b_{2} being object st x = [b_{1},b_{2}]

then ex i being Element of NAT st

( x = [i,(i + 1)] & i + 1 < n ) ;

hence ex b_{1}, b_{2} being object st x = [b_{1},b_{2}]
; :: thesis: verum

end;assume x in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } ; :: thesis: ex b

then ex i being Element of NAT st

( x = [i,(i + 1)] & i + 1 < n ) ;

hence ex b

set B = n -SuccRelStr ;

deffunc H

deffunc H

defpred S

set R = { [H

A1: I = { [H

A2: I ~ = { [H

the InternalRel of (n -SuccRelStr) = I by Def6;

hence the InternalRel of (Necklace n) = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } \/ { [(i + 1),i] where i is Element of NAT : i + 1 < n } by A2, Def7; :: thesis: verum