let n be Nat; :: thesis: ( n > 0 implies card the InternalRel of (Necklace n) = 2 * (n - 1) )
assume A1: n > 0 ; :: thesis: card the InternalRel of (Necklace n) = 2 * (n - 1)
then A2: n >= 0 + 1 by NAT_1:13;
deffunc H₁( Element of NAT ) -> Element of NAT = $1;
deffunc H₂( Element of NAT ) -> Element of NAT = $1 + 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] } ;
A3: 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 Th19;
{ [i,(i + 1)] where i is Element of NAT : i + 1 < n } = the InternalRel of (n -SuccRelStr ) by Def7;
then A4: card { [i,(i + 1)] where i is Element of NAT : i + 1 < n } = n - 1 by A1, Th17;
A5: card { [H₂(i),H₁(i)] where i is Element of NAT : S₁[i] } = n - 1 by A1, Th27;
{ [i,(i + 1)] where i is Element of NAT : i + 1 < n } is Relation-like

proof

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

end;

then reconsider A = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } as Relation ;
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 set 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 set such that
A11: x = [y,z] by A9, RELAT_1:def 1;
A12: [z,y] in A by A7, A10, A11, RELAT_1:def 7;
consider i being Element of NAT such that
A13: ( [y,z] = [i,(i + 1)] & i + 1 < n ) by A9, A11;
A14: ( y = i & z = i + 1 ) by A13, ZFMISC_1:33;
consider j being Element of NAT such that
A15: ( [z,y] = [j,(j + 1)] & j + 1 < n ) by A12;
( z = j & y = j + 1 ) by A15, ZFMISC_1:33;
hence contradiction by A14; :: thesis: verum

end;

A16: n -' 1 = n - 1 by A2, XREAL_1:235;
card the InternalRel of (Necklace n) = (card (n - 1)) +` (card (n - 1)) by A3, A4, A5, A8, CARD_2:48
.= card ((n -' 1) + (n -' 1)) by A16, CARD_2:51
.= 2 * (n - 1) by A16, CARD_1:def 5 ;
hence card the InternalRel of (Necklace n) = 2 * (n - 1) ; :: thesis: verum