let n be Nat; :: thesis: ( n > 0 implies card the InternalRel of (Necklace n) = 2 * (n - 1) )
deffunc H₁( Element of NAT ) -> Element of omega = $1 + 1;
deffunc H₂( Element of NAT ) -> Element of NAT = $1;
defpred S₁[ Element of NAT ] means $1 + 1 < n;
set A = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } ;
set B = { [H₁(i),H₂(i)] where i is Element of NAT : S₁[i] } ;
A1: { [i,(i + 1)] where i is Element of NAT : i + 1 < n } is Relation-like

proof

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₁, b₂ being object st x = [b₁,b₂] )
assume x in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } ; :: thesis: ex b₁, b₂ being object st x = [b₁,b₂]
then ex i being Element of NAT st
( x = [i,(i + 1)] & i + 1 < n ) ;
hence ex b₁, b₂ being object st x = [b₁,b₂] ; :: thesis: verum

end;

A2: the InternalRel of (Necklace n) = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } \/ { [H₁(i),H₂(i)] where i is Element of NAT : S₁[i] } by Th17;
assume A3: n > 0 ; :: thesis: card the InternalRel of (Necklace n) = 2 * (n - 1)
then n >= 0 + 1 by NAT_1:13;
then A4: n -' 1 = n - 1 by XREAL_1:233;
{ [i,(i + 1)] where i is Element of NAT : i + 1 < n } = the InternalRel of (n -SuccRelStr) by Def6;
then A5: card { [i,(i + 1)] where i is Element of NAT : i + 1 < n } = n - 1 by A3, Th15;
reconsider A = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } as Relation by A1;
A6: A = { [H₂(i),H₁(i)] where i is Element of NAT : S₁[i] } ;
A7: A ~ = { [H₁(i),H₂(i)] where i is Element of NAT : S₁[i] } from NECKLACE:sch 1(A6);
A8: A misses { [H₁(i),H₂(i)] where i is Element of NAT : S₁[i] }

proof

assume A meets { [H₁(i),H₂(i)] where i is Element of NAT : S₁[i] } ; :: thesis: contradiction
then consider x being object such that
A9: x in A and
A10: x in { [H₁(i),H₂(i)] where i is Element of NAT : S₁[i] } by XBOOLE_0:3;
consider y, z being object such that
A11: x = [y,z] by A9, RELAT_1:def 1;
[z,y] in A by A7, A10, A11, RELAT_1:def 7;
then consider j being Element of NAT such that
A12: [z,y] = [j,(j + 1)] and
j + 1 < n ;
A13: ( z = j & y = j + 1 ) by A12, XTUPLE_0:1;
consider i being Element of NAT such that
A14: [y,z] = [i,(i + 1)] and
i + 1 < n by A9, A11;
( y = i & z = i + 1 ) by A14, XTUPLE_0:1;
hence contradiction by A13; :: thesis: verum

end;

card { [H₁(i),H₂(i)] where i is Element of NAT : S₁[i] } = n - 1 by A3, Th25;
then card the InternalRel of (Necklace n) = (card (n - 1)) +` (card (n - 1)) by A2, A5, A8, CARD_2:35
.= card ((n -' 1) + (n -' 1)) by A4, CARD_2:38
.= 2 * (n - 1) by A4 ;
hence card the InternalRel of (Necklace n) = 2 * (n - 1) ; :: thesis: verum