let n be Nat; ( not Necklace n, ComplRelStr (Necklace n) are_isomorphic or n = 0 or n = 1 or n = 4 )
assume A1:
Necklace n, ComplRelStr (Necklace n) are_isomorphic
; ( n = 0 or n = 1 or n = 4 )
set S = Necklace n;
set T = ComplRelStr (Necklace n);
card n = n
;
then A2:
card [:n,n:] = n * n
by CARD_2:46;
assume A3:
( not n = 0 & not n = 1 & not n = 4 )
; contradiction
( n <= 4 implies not not n = 0 & ... & not n = 4 )
;
then
( n = 2 or n = 3 or n > 4 )
by A3;
then A4:
card the InternalRel of (Necklace n) = 2 * (n - 1)
by Th26;
A5:
((n * n) - (2 * (n - 1))) - n <> 2 * (n - 1)
A8:
id the carrier of (Necklace n) misses the InternalRel of (Necklace n)
the carrier of (Necklace n) = n
by Th19;
then A14:
card ( the InternalRel of (Necklace n) `) = (n * n) - (2 * (n - 1))
by A4, A2, CARD_2:44;
( the carrier of (Necklace n) = n & n = card n )
by Th19;
then A15:
card (id the carrier of (Necklace n)) = n
by Th4;
card the InternalRel of (ComplRelStr (Necklace n)) =
card (( the InternalRel of (Necklace n) `) \ (id the carrier of (Necklace n)))
by Def8
.=
((n * n) - (2 * (n - 1))) - n
by A14, A15, A8, CARD_2:44, XBOOLE_1:86
;
hence
contradiction
by A1, A4, A5, Th16; verum